Since we already have Separation, it’s enough to show the following:

if $\phi$ is a functional formula and $x\in M[G]$, then there is $R\in M[G]$ such that

$$M[G]\models \forall y\in x,\exists z\in R,\phi (y,z,\cancel{\overline{p}})\text{(∗)}$$

(as before, we suppress parameters for notational ease).

We work in $M$ and identify a name $\rho$ for $R$. Fix $\sigma$ such that $x=\mathrm{val}(\sigma ,G)$. Find $\alpha$ large enough such that $\mathrm{dom}(\sigma )\subseteq V_{\alpha }$. Consider $\psi (p,\pi ):=\exists \mu ,p⊩\phi (\pi ,\mu )$ ($p\in \mathbb{P}$, $\pi$ a name). By Definability Theorem, this is an $L_{\in }$ formula.

By Levy Reflection Theorem, find $𝜃>\alpha$ such that $\psi$ is absolute between $V_{𝜃}$ and $V=M$. Define

$$\rho :=\{(\mu ,1):\mu \in V_{𝜃}\}$$

and $R:=\mathrm{val}(\rho ,G)$.

Now we verify ($\ast$) holds: Fix $y\in x$, $y=\mathrm{val}(\pi ,G)$. Since $\phi$ is functional, we know that $\phi (\pi ,\mu )$ holds in $M[G]$ for some $\mu$. By Forcing Theorem, there is $p\in G$ such that $p⊩\phi (\pi ,\mu )$. So $M\models \psi (p,\pi )$.

By absoluteness, $V_{𝜃}\models \psi (p,\pi )$. This means $\exists \mu \in V_{𝜃}$ such that $p⊩\phi (\pi ,\mu )$.

Thus: $\mathrm{val}(\mu ,G)\in \mathrm{val}(\rho ,G)=R$.