Proving Separation from Replacement

You can see in Stanford Encyclopedia of Philosophy the entry on Set Theory .

The Supplement listing the axioms of Zermelo-Fraenkel Set Theory has :

The final axiom of $\mathsf {ZF}$ is the Replacement Schema. Suppose that $\phi(x,y,û)$ is a formula with $x$ and $y$ free, and let $û$ represent the variables $u_1,…,u_k$, which may or may not be free in $\phi$. Furthermore, let $\phi_{x,y,û}[s,r,û]$ be the result of substituting $s$ and $r$ for $x$ and $y$, respectively, in $\phi(x,y,û)$. Then every instance of the following schema is an axiom:

Replacement Schema:

$\forall u_1 …\forall u_k [\forall x \exists !y \phi(x,y,û) \rightarrow \forall w \exists v \forall r (r \in v \equiv \exists s(s \in w \land \phi_{x,y,û}[s,r,û]))]$

In other words, if we know that $\phi$ is a functional formula (which relates each set $x$ to a unique set $y$), then if we are given a set $w$, we can form a new set $v$ as follows: collect all of the sets to which the members of $w$ are uniquely related by $\phi$.

Note that the Replacement Schema can take you ‘out of’ the set $w$ when forming the set $v$. The elements of $v$ need not be elements of $w$. By contrast, the well-known Separation Schema of Zermelo yields new sets consisting only of those elements of a given set $w$ which satisfy a certain condition $\psi$. That is, suppose that $\psi(x,û)$ has $x$ free and may or may not have $u_1, …,u_k$ free. And let $\psi_{x,û}[r,û]$ be the result of substituting $r$ for $x$ in $\psi(x,û)$. Then the Separation Schema asserts:

Separation Schema:

$\forall u_1 …\forall u_k[\forall w \exists v \forall r(r \in v \equiv r \in w \land \psi_{x,û}[r,û])]$

In other words, if given a formula $\psi$ and a set $w$, there exists a set $v$ which has as members precisely the members of $w$ which satisfy the formula $\psi$.

A formal proof of the relation between the two is in Gaisi Takeuti & Wilson Zaring, Introduction to Axiomatic set theory (1971), page 17 (we omit the initial string of $\forall$s) :

Axiom Schema of Replacement

$\forall a [\forall u \forall v \forall w [\phi(u, v) \land \phi(u, w) \rightarrow v = w] \rightarrow \exists b \forall x [x \in b \equiv \exists u [u \in a \land \phi(u, x)]]]$.

Note. The condition of functionality for $\phi$ has been unwinded.

Note also that $a$ is not mentioned in the antecedent, so you can rewrite the formula as : $\forall u \forall v \forall w [...] \rightarrow \forall a\exists b \forall x [x \in b \equiv \exists u [u \in a \land \phi(u, x)]]$. In this way, the consequent has clearly the "form" of Separation.

Zermelo's Schema of Separation

$ \forall a \exists b \forall x [x \in b \equiv x \in a \land \phi(x)]$.

Applying Replacement to the wff $\phi(u) \land u = v$ where $v$ does not occur in $\phi(u)$ we have that $[\phi(u) \land u=v] \land [\phi(u) \land u=w] \rightarrow v = w$.

Note. After an "instantiation" of the Replacement schema, the universal closure of the above formula give us its antecedent ; so we can "detach" the consequent.

Therefore

$\exists b \forall x [x \in b \equiv \exists u [\phi(u) \land u = x \land x \in a]]$

i.e. [Note: here we have several steps in one; we need the equality axiom $\vdash u = x \rightarrow (\phi(u) \rightarrow \phi(x))$, "rearranged" as $\vdash (\phi(u) \land u = x ) \rightarrow \phi(x)$ and a final application of quantifier rules to get : $\vdash \exists u(\phi(u) \land u = x ) \rightarrow \phi(x)$.]

$\exists b \forall x [x \in b \equiv \phi(x) \land x \in a]$.

Note. The final step is to introduce the universal quantifier $\forall a$, by "generalization".