If the axiom of replacement implies the axiom of specification, why are both mentioned In Tao's Book on Analysis I, we are asked to prove that the axiom of replacement implies the axiom of specification.
This implication seems to be true even outside of the environment Tao sets up in his book, as I've seen it mentioned elsewhere.
During my own quest into the foundations-of-mathematics jungle, I've come across the more standard lists for the Zermelo-Fraenkel Axioms of set theory, and they all seem to mention both of these axioms.
My question is simply, if one implies the other, and the goal of an axiomatization is to find the fewest number of comprehensible axioms, then why are both of them listed? Is it solely to show that specification is also possible? Or is it because this implication is based on some other tacitly assumed truth. None of the above?
 A: Two reasons, one historical and one technical.
The historical reason is that when Zermelo first formulated the axioms of set theory (Zermelo set theory), Replacement was not an axiom. That was Fraenkel's contribution later on, giving us the more familiar ZF axioms. (Well technically Skolem/von Neumann also contributed the axiom of regularity).
The technical reason is that in set theory one often considers structures that satisfy some partial collection of the ZFC axioms. For example, the limit stages of the von Neumann hierarchy satisfy all the ZFC axioms except Replacement. So we can say pretty succinctly that they satisfy ZFC minus Replacement, instead of the more mouthful "they satisfy ZFC minus Replacement plus Specification".
A: The abridged version of Replacement in [1] is $\forall X (\;[\forall x\in X\exists! y (F(x,y))]\implies [\exists Z\forall x\in X\forall y( F(x,y)\implies y\in Z]\;)$ where $F(x,y)$ is a formula whose free variables, if it has any, are $x$ or $y$ or both.
We can then take the set $Z$ and apply Comprehension to get $Y=\{y\in Z: \exists x\in X(F(x,y))\}$, that is, to get $\forall X (\; [\forall x\in X\exists! y (F(x,y))]\implies [\exists Y\forall x\in X\forall y( F(x,y)\iff y\in Y)]\;)$ .
The versions of C and R in [1] are independent. However, Godel showed that that if you take ZF minus Comprehension (C) (with R as in [1]) then C is equivalent to one axiom rather than an infinite schema of axioms (This is not covered in [1]). He actually presented it as the conjunction of 8 axioms instead of as one rather long sentence.
BTW, erasing the "$!$" from R is equivalent to adding the Axiom of Choice (AC).
Reference. [1]. Kunen, Kenneth. Set Theory: An Introduction To Independence Proofs.
