By the axiom schema of collection in ZF, I mean: $$\forall A \exists B \forall x \in A (\exists y \phi(x,y) \to \exists y \in B \phi(x,y))$$, for every formula $\phi$ that doesn't use the symbol $B$.
On the other hand the axiom schema of replacement states that if $\phi$ is a first-order formula, and $A$ is a set such that for any $x\in A$ there exists a unique $y$ such that $\phi(x,y)$, then there exists a set $B$ such that $y\in B$ if and only if $\phi(x,y)$ for some $x\in A$. That is, $B$ is the "image" of $A$ under the "definable class function" $\phi$. [Quoted from here]
The proof that I know of uses Regularity. We replace each element $x$ of $A$ by the minimal stage of the cumulative hierarchy that has an element $y$ that satisfy $\phi(x,y)$, then we take the union of the resulting set.
I'm personally not aware of another proof of collection in ZF. Since the above proof clearly depends on Regularity, hence my question:
Is collection scheme provable in ZF-Regularity?
In other words, is there a model of ZF-Regularity in which collection fails?
