Replacement in L

The fixed ambient formula $y\in L\wedge {\varphi }^L(x,y,p)$ is functional on the actual set $a$, since transitivity puts each $x\in a$ in L. Ambient Replacement therefore forms its image Y as a set of constructible elements. Ambient Replacement again forms the set of their constructible ranks. A successor above their supremum and the finitely many parameter ranks gives $\beta$ with $Y\subseteq L_{\beta }$ and $a,p_i\in L_{\beta }$. Empty images require no exception to this bound.

Apply Separation inside L to the set $L_{\beta }\in L$ with formula $\mathrm{\exists }x\in a\varphi (x,y,p)$. Its relativization singles out exactly Y, because step 1.1 bounded the entire image. Hence $Y\in L$, using neither internal Replacement nor a choice of witnesses.

Equivalently, reflect that fixed image-defining formula at a level $L_{\gamma }$ above $\beta$. All image elements and parameters are in this level. Agreement makes its Def subset precisely Y, so $Y\in L_{\gamma +1}$. This also confirms that the assertion is a scheme for fixed formulas and has no uniform class-truth premise.