Can ZF be interpreted in a theory axiomatized by a version of replacement and infinity?

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}$.

• You might want to take a look at Harvey Friedman's manuscript "Axiomatization of Set Theory by Extensionality, Separation and Reducibility", found on his homepage under the "Downloadable Lecture Notes" section to see what can happen when one removes certain axioms from $ZF$. Very interesting. – Thomas Benjamin Jan 19 at 11:51
• Yes, it is interesting, I remember I read his dual world approach with his axiom of reducibility. It is nice. – Zuhair Al-Johar Jan 19 at 20:41