Dana Scott had once proved that Zermelo's set theory $``\text{Z}"$ can be interpretable in the first order set theory whose axioms are just the axioms of:

1. Separation: if $\phi$ is a formula in which x doesn't occur, then:
   $\forall A \exists x \forall y (y \in x \iff y \subset A \wedge \phi)$
   is an axiom.
2. Infinity: the usual form

Can a similar situation occur with $\text{ZF}$, i.e. can we have a theory whose axiomatic system consists of a modified form of Replacement and an Infinity axiom, that can interpret $\text{ZF}$? Here is a try:

1. Replacement: if $\phi(x,y)$ is a formula in which the symbols $``x"$, $``y"$ occur free, and those never occur bound, and in which the symbol $``B"$ never occur, then: $\forall A ([\forall x \in A \exists z \forall y (\phi(x,y) \implies y \subset z) ]\implies \exists B \forall y (y \in B \iff \exists x \in A \phi(x,y)))$
   is an axiom.

2. Infinity: the usual form.

/

The idea is that this form of Replacement do prove Pairing, Power, Separation and the form of axiom schema of replacement I've lately posted to Mathoverflow at:

Equivalents of Replacement under removal of Extensionality?

and it would prove Union over sets in which every element of them is an element of some transitive set.

This seems to be enough to interpret the cumulative hierarchy and thus full $\text{ZF}$.