In Kanamori's [Bernays and Set Theory](https://www.researchgate.net/publication/220366286_Bernays_and_Set_Theory) pages 20-21, a first order reflection principle due to Bernays is mentioned, that of:



> 
> $$\sf \varphi \to \exists y \, (\text {Trans}(y) \land \varphi^y)$$ for formulas $\varphi$ without $\sf y$ or any class variables, where $\sf Trans(y) $ asserts that $\sf y$ is transitive; $\sf \varphi ^ y$ denotes the relativization of the formula $\varphi$ to the set $\sf y$, i.e., $\exists x$ is replaced by $\exists x \in \sf y$ and $\forall x$ by $\forall x \in \sf y$. Starting with the observation that set parameters $a\_1,...,a\_n$ can
> appear in $\varphi$ and $\sf y$ can be required to contain them by introducing clauses $\exists x(a\_i \in x)$ into $\varphi$. Bernays just with his schema established Pair, Union, Infinity, and Replacement (schema)—in effect achieving a remarkably economical presentation of ZF.
> 
> 
> 


My question: what is the proof of replacement from reflection?
It's easy to see that Reflection can prove Pairing, Union, and Infinity. But the proof of Replacement is what's escaping me.


I tried to reflect the formula: $\exists x (a \in x) \land \forall m \in a \exists ! z: \phi(m,z)$ on the transitive set $\sf y$, but what we'll get is a set (which is $\sf y$) that contains the $z$'s of $\phi^\sf y$ among its elements, and I don't know how those are the same $z$'s of $\phi$?



What is the proof of replacement from Bernays first order reflection?
The above reflection scheme does not imply the existence of an empty set, nor does it imply the existence of more than one element. In the domain with one element which is an element of itself, the reflection scheme holds.


Let T0 be the theory whose axioms are extensionality, foundation and the above reflection scheme. If ZF is consistent, then pairing, union, power set and some instances of separation are not provable from T0.


Proof:Let A=ωU{{1},{{1}}}. Let U(y) be a formula which holds iff y∈A or (y∉Vω and for every x∉Vω which is in the transitive closure of {y}, the intersection of Vω with the transitive closure of x is A).


Then relativized to U, the above reflection scheme holds, but pairing, union, some instances of separation, and power set do not.


Let T1 be the theory whose axioms are the axioms of T0, power set, and all instances of separation. Then if ZF is consistent, there are instances of replacement not provable from T1.


Proof: Define a sequence s by s0=0, and s(n+1)=U{b|there is a "formula with parameters from V(sn) such that b is the least ordinal for which holds in Vb"}


Let t=U{sn| n∈ω}. Then all the axioms of T1 hold in Vt, but there are instances of replacement that do not. For example,


let ψ(n,x) be a formula which holds iff n∈ω and x=sn.


