Why do we allow redundant axioms in ZFC? I learned recently that even though ZFC is often said to have nine axioms, there are only 7 independent axioms (actually, 6 axioms and one axiom schema). These seven axioms are listed here. In summary, the following statements, often listed as axioms, are redundant:
"Axiom" of Empty Set: There exists a set with no elements.
"Axiom" of Pairing: If $a$ and $b$ are sets, there exists the set $\{a,b\}.$
"Axiom" of Specification: If $A$ is a set and $P(x)$ a proposition for each $x\in A$, then $\{x\in A|P(x)\}$ is a set.
Most sources I've seen include two of the above redundant axioms, giving a total of nine. 
Why do we ever consider these sets of statements to all be axioms if some are redundant?
The answer here cites "convenience" as the reason, but this is nonsense. It would be just as convenient to call the redundant facts "theorems" and cite them as theorems when using them in other proofs. (Unless the "convenient" part is ignoring the proofs that they are redundant. But then it would be just as convenient to call the redundant facts "theorems" and not prove them, and at least that would be more transparent!)
There are some interesting discussions on math.SE, such as here, about the different meanings of "axiom." I can understand the word might have picked up different meanings/connotations in different areas (group axioms simply define a group, whereas set theory axioms declare "self-evident truths" about sets, according to some). But the concept of redundant axioms seems totally incoherent. Didn't several mathematicians spend their whole lives trying to show that Euclid's fifth postulate was redundant so that they could eliminate it from the list? If we accept all nine statements as axioms, why not accept all theorems of set theory as axioms?
 A: There is in fact considerable variation in how the axioms of ZFC are defined.  Different authors give different exact statements of several of the axioms.  Some authors omit some of the axioms which are redundant.
The point is that for most purposes, we don't care about the individual axioms.  We only care about the theory that they generate: that is, which theorems we can prove from the axioms*.  That's the main point of a foundation for math: it gives a precisely defined notion of "theorem" that everyone can agree on.  So, no one will care if you use a funny version of ZFC which includes some statements as axioms which to you are theorems or omits some of your axioms, as long as it ends up proving the same theorems overall.  Assuming you know that certain sets of axioms are equivalent to each other, the reason you would pick one over another is convenience: one may be easier for your audience to understand, for instance, or may just be traditional for historical reasons.
You seem concerned about choosing a foundation for math that involves as few assumptions as possible.  That is reasonable, but if you can prove that certain assumptions are equivalent to other assumptions, that means it no longer really matters which of them you use; they have the exact same logical content, just expressed in different ways.
*We also care about there being an algorithm that identifies whether a proof from our axioms is valid.  However, this will be true for any remotely reasonable choice of axioms.
