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](https://cpb-us-w2.wpmucdn.com/u.osu.edu/dist/1/1952/files/2014/01/TalkAxiomSetThy-ts05xn.pdf) he didn't cite a reference to that result.



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



Reference request: for a proof of a reflection [from transitive sets] based axiomatization of ZF\Reg.?
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.


