Independence of the Axiom of Separation Consider ZFC with the Axiom of Replacement formulated as
$$ \forall x\forall y\forall z(\phi(x,y)\land \phi(x,z)\to y=z) \to \forall a\exists w\forall x\forall y(x\in a\land \phi(x,y)\to y\in w) $$
where $\phi$ is a two-place predicate that may contain parameters not among $a, x, y, z, w$. The difference from the usual Replacement is that it may produce a superset of the range of $\phi$.
For my purposes here, ZFC includes the Axiom of Regularity, and the null set, pairing, union, and power set axioms do give exact results.
In the presence of the Axiom of Separation, the weakened Replacement axiom easily implies the exact version; conversely the full Replacement by itself implies Separation.
However, the weak Replacement does not seem to imply Separation. Is there a nice way to prove this?
More precisely, let FC be ZFC as sketched above, without Separation. Does ZFC prove that FC is consistent?

If we didn't have to satisfy Regularity, it would be easy: Let the universe be $\mathbb N$, and let $n\in m$ mean "$m=0$ or the $n$th bit in the binary representation of $m-1$ is 1". Then $0$ would represent a universal set, which would immediately satisfy the weakened Replacement as well as Infinity. But this model would fail Regularity due to the universal set (and its singleton). And without a universal set it seems to be hard to be sure you've tamed all possible instances of the weak Replacement.
 A: The following class-sized model in ZFC works, I think. (And I would guess that a set-sized version could be constructed in ZFC). 
Let:
$\mathcal M_0 = \emptyset$
$\mathcal M_{\alpha+1} = \mathcal M_\alpha \cup\{\mathcal M_\alpha\}\cup \{\{x,y\}:x,y \in \mathcal M_\alpha\} \cup \{\cup x:x\in\mathcal M_\alpha\}\cup\{\{y\subseteq x: y\in \mathcal M_\alpha\}:x\in\mathcal M_\alpha\}\cup \{y\subseteq \mathcal M_\alpha\cap x\times x: x\in\mathcal M_\alpha \wedge \mbox{$y$ is a well-order of $x$}\}$
$\mathcal M_\lambda = \bigcup_{\alpha<\lambda} \mathcal M_\alpha$
It is easy to see that $\mathcal M_\Omega = \bigcup \mathcal M_\alpha$ satisfies Infinity, Pairing, Union, Foundation, and Choice. For Powerset, note that the subsets of $x$ have to all occur in some $\mathcal M_\alpha$. Similarly for Replacement. 
Now a simple induction establishes that the transitive closure of every set in $\mathcal M_\Omega$ either contains finitely many finite ordinals or infinitely many non-ordinals. So it does not contain $\omega$, even though $\omega$ is $\Delta_0$ definable over $\mathcal M_\omega = V_\omega$. 
