I'm trying to show that separation follows from replacement. There are at least two questions here on SE that deal with the question. See The comprehension axioms follows from the replacement schema. and How do the separation axioms follow from the replacement axioms?. I'm not completely satisfied with the answers there.
The basic idea for the proof that most people use seems to be this: Say we have some set $D$ and some formula $\varphi(x)$. To prove separation, we're trying to show that $\{x \in D| \varphi(x)\}$ is a set. Using separation, we need to write a formula $\psi(x,y)$ such that for each $x \in D$ there is exactly one $y$ such that $\psi(x,y)$.
Here's one attempt: $\psi(x,y) = \text{"}x = y \wedge \varphi(x) \text{''}$. IF this formula satisfies the separation axiom, THEN this should work fine. The problem: at least in the version of the separation axiom I know, we need for there to be a unique $y$ for all $x \in D$, such that $\psi(x,y)$. So say $x \in D$ is such that $\neg \varphi(x)$, then $\psi(x,y)$ is always false (and so not true for a unique $y$ as required for the use of replacement).
Here's another attempt: $\psi(x,y) = \text{''}(\{x\}=y \wedge \varphi(x))\vee y=\emptyset \text{''}.$ Now we have a function whose domain is the entire set $D$. And we can use replacement and union to get the set we want. But this requires that both $\emptyset$ and $\{x\}$ are sets. This is the usual argument that they are sets. $D$ is a set, so $\{x \in D| x \not = x\}=\emptyset$ is a set. But that's a straightforward use of separation. We have the same problem for $\{x\}$. Using pairing we get that there is a set $A$ such that $x \in A$, but we don't necessarily have as a result that there is a set that contains only $x$. Of course we could construct this set with $\{y \in A | y = x\}$, but again we've used separation.
It's for the reasons above that I'm not perfectly satisfied with the answers to other questions here on SE. Perhaps I've made some mistake, or there actually is a better answer.
Best Answer
You can see in Stanford Encyclopedia of Philosophy the entry on Set Theory .
The Supplement listing the axioms of Zermelo-Fraenkel Set Theory has :
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) :
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.
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".