Reference request: for a proof of a reflection [from transitive sets] based axiomatization of ZF\Reg.?

Question

The following system is quoted from Harvey Friedman's lecture notes. The language is first order logic with membership $\in$.

Axioms:

1. Extensionality. $(\forall x)(x \in y \leftrightarrow x \in z) \to (\forall x)(y \in x \leftrightarrow z \in x).$

2. Pairing. $(\exists x)(y,z \in x).$

3. Union. $(\exists x)(\forall y \in w)(\forall z \in y)(z \in x).$

4. Separation. $(\exists x)(\forall y)(y \in x \leftrightarrow (y \in z \land \varphi))$, where $\varphi$ is a formula in $L(\in )$ in which $x$ is not free.

5. Power set. $(\exists x)(\forall y)(y \subseteq z \to y \in x).$

6. Reflection. $(\exists \ transitive \ x)(y_1,…,y_n \in x \land (\forall z_1,…,z_m \in x)((\exists w)(\varphi) \to (\exists w \in x)(\varphi)))$, where $m,n \geq 1$ and $\varphi$ is a formula in $L(\in )$ whose free variables are among $y_1,…,y_n,z_1,…,z_m,w.$

7. Infinity. $(\exists x)(\emptyset \in x \land (\forall y \in x)(y \cup \{y\} \in x)).$

This system is equivalent to $\small \sf ZF\setminus Reg.$ according to H. Friedman. However in his lecture notes he didn't cite a reference to that result.

Question: Where can I find a proof of this result?

Answer 1

This was actually a result I used in a paper I am working on.

Let $M$ reflect $\exists x(x\in X\land\phi(x,y))$ (In this case $\phi(x,y)↔y=f(x)$). Then $\{y│(M,∈)\vDash\exists x(x\in X\land\phi(x,y))\}=\{y│\exists x(x\in X\land\phi(x,y))\}\cap M$ and $\{y│\exists x(x\in X\land\phi(x,y))\}\cap M=\{y│\exists x(x ∈ X\land\phi(x,y))\}$. Therefore $\{y│\exists x(x ∈ X\land\phi(x,y))\}\subseteq M$. By separation then $\{y│\exists x(x ∈ X\land\phi(x,y))\}$ is a set.