Power-set axiom in the constructible universe
= Power-set axiom in the constructible universe
{title2=$\mathcal P^L(a)=\mathcal P^V(a)\cap L\in L$}
For $a\in L$, ambient <separation> forms $S=\mathcal P(a)\cap L$. Ambient <replacement> bounds the first constructible stages of all members of $S$. At a stage containing $a$ and all of $S$, the latter is definable by the bounded property of being a <subset> of $a$. Thus $S$ belongs to the next constructible stage and is the internal <power set> in $L$.