Relativized closure criterion for separation (source code)

= Relativized closure criterion for separation

Let $M$ be a transitive class. If $M$ is closed under the ambient subsets defined by $\varphi^M$, then $M$ satisfies the $\varphi$-instance of separation, because
$$
\{z\in x:V\models\varphi^M(z)\}
=\{z\in x:M\models\varphi(z)\}.
$$