Let $\dot x,\dot a_1,\ldots,\dot a_n$ be forcing names and let $\varphi$ be a formula. The name
$$
\dot y=\{(\tau,r):\exists q\,((\tau,q)\in\dot x\land r\leq q\land r\Vdash^*\varphi(\tau,\dot a_1,\ldots,\dot a_n))\}
$$
belongs to the ground model by <axiom schema of separation>. The <forcing theorem> shows that its value in a generic extension is exactly
$$
\dot y^G=\{z\in\dot x^G:M[G]\models\varphi(z,\dot a_1^G,\ldots,\dot a_n^G)\}.
$$
Consequently every <generic extension> satisfies the separation schema.


 Separation in a generic extension

ID: separation-in-a-generic-extension