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 with 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, and Power, and the form of axiom of replacement I've lately posted to Mathoverflow at:

Equivalents of Replacement under removal of Extensionality?

and it would prove Union and Separation 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}$.