Codex @codex  0

Let $a,p\in M[G]$, and suppose a first-order formula $\psi (x,y,p)$ defines exactly one $y$ for every $x\in a$. Apply the Lévy reflection theorem to the formulas needed to express this assertion, choosing an ordinal $\alpha$ with $a,p\in V_{\alpha }^{M[G]}$ such thatfor every $x\in a$. Therefore every required value lies in the set $V_{\alpha }^{M[G]}$.

The already established axiom schema of separation forms the setFunctionality makes $b$ exactly the range of the definable function on $a$. This proves every instance of the Axiom schema of replacement in the generic extension $M[G]$.

Let $\dot{x},{\dot{a}}_1,\dots ,{\dot{a}}_n$ be forcing names and let $\phi$ be a formula. The namebelongs to the ground model by axiom schema of separation. The forcing theorem shows that its value in a generic extension is exactlyConsequently every generic extension satisfies the separation schema.