Using the Reflection Theorem I've been reading about the Reflection Theorems in Kunen's 2011 Set Theory book. The idea that $ZFC \not \vdash \exists \gamma [V_\gamma \models ZFC]$, but $ZFC \vdash \exists \gamma [V_\gamma \models ZC \cup \Lambda]$ for a finite list $\Lambda$ of instance of the Replacement Axiom seemed really interesting. 
After proving this result with transitive models, Kunen mentions that we can also let $\Lambda$ be a finite set of sentences. However, he mentions that we run into difficulty when we use formulas and that we can't generally get this statment to be true. He then gives an exercise to show an instance of when this is true.

Assume the Axiom of Choice. Find a formula $\varphi$ such that every transitive $M$ satisfying $M \preccurlyeq_{\varphi} V$ is of the form $V_\gamma$ for some $\gamma = \beth_\gamma$.

He also gives a hint: $\varphi$ can be $\varphi_0(x) \wedge \varphi_1$, where $\varphi_0(x)$ says that $x$ is the set of the form $V_\alpha$, and $\varphi_1$ is a sentence and a theorem of $ZFC$.
I'm having difficulty with this problem. In particular, understanding the hint. Also, I know some facts about the Beth function $\beth_\gamma$, but I'm not sure why it's being used. Any help/hints would be greatly appreciated.
 A: Recall that for all sets $x$ and all ordinals $\alpha$ we have that $rank(x)=\alpha$ if and only if there is an onto homomorphism $f:(trcl(x),\in)\longrightarrow(\alpha,\in)$. Also for all sets $x,y$, $y=trcl(x)$ if and only if $y$ is transitive, $x\subseteq y$, and for all transitive sets $z$ such that $x\subseteq z$ we have $y\subseteq z$. Also for all $\alpha$, $|V_\alpha|=\beth_\alpha$.
Define $\psi_1(x,y)=\exists z(z$  is an onto homomorphism from $(x,\in)$ onto $(y,\in));$ informally, $z(x_1)\in z(x_2)$ whenever $x_1\in x_2$ in $x$. 
Let $\psi_2(x,y)=(y$ is transitive $\wedge x\subseteq y)\wedge\forall z(z$ is transitive $\wedge x\subseteq z\rightarrow y\subseteq z)$, so, informally, $\psi_2(x,y)$ tells that $y$ is the transitive clousure of $x$; for transitive models.
Let $\psi_3(x,y)=y$ is an ordinal $\wedge\forall w\in x(\exists w'\in y\exists z(\psi_2(w,z)\wedge\psi_1(z,w'))\wedge\forall z(\exists w'\in y\exists z'(\psi_2(z,z')\wedge\psi_1(z',w')\rightarrow z\in x)),$ then $\psi_3(x,\alpha)$ "says" $x=V_\alpha^M.$ Let $\psi(x)=\exists\alpha\varphi(x,\alpha)$. Put $\sigma_1=\forall y\exists x(\psi(x)\wedge y\in x)$ and $\sigma_2=\forall y(y$ is an ordinal$\leftrightarrow\exists x(\psi_3(x,y)))$
Finally put $\sigma_3=\forall\alpha(\alpha$ is ordinal$\rightarrow\exists\gamma\exists x(\alpha\in\gamma\wedge\gamma$ is an ordinal$\wedge \psi_3(x,\gamma)\wedge |\gamma|=|x|)),$ this will imply that as $x=V_{\gamma}^M$, then $\beth_{\gamma}^M=\gamma$.
Put $\varphi(x)=\sigma_1\wedge\sigma_2\wedge\sigma_3\wedge\psi(x).$ 
Let $M$ be a transitive set such that $M\preceq_{\varphi(x)}V$. Put $\gamma=M\cap ON$. Then $\sigma_1\wedge\sigma_2\wedge\sigma_3$ is a theorem of $\mathsf{ZFC}$. Let $M$ be transitive set such that $(M,\in)\preceq_{\varphi(x)} V.$ As $M\preceq_{\sigma_2}V$ and the notion of being an ordinal is absolute for $M$, we obtain that for all $x\in M$, $V_x^M$ is defined if and only if $x$ is an ordinal $<$ $\gamma$. Also $M\preceq_{\sigma_1}V,$ this implies that $M=\bigcup_{\alpha<\gamma}V_\alpha^M.$ Finally, $M\preceq_{\psi(x)} V$ implies that for all $\alpha<\gamma,V_{\alpha}$ is absolute for $M$, in consequence $M=\bigcup_{\alpha<\gamma} V_\alpha$.
As $M\preceq_{\sigma_3} V$, and both the notion of being an ordinal and $V_\alpha$ are absolute for $M$, $\alpha<\gamma$, we obtain that $\forall\alpha<\gamma\exists\beta<\gamma[\alpha<\beta\wedge\beta=\beth_\beta],$ this implies that $\gamma$ is a limit ordinal and furthermore $\gamma=\beth_\gamma$, thus $M=\bigcup_{\alpha<\gamma} V_\alpha=V_\gamma$.
Notice that the only part of the answer where choice was used was for $\beth_{\alpha}$ to be defined.
