= Solution
Fix $a\in L$. In the ambient universe form the <set>
$$
S=\{y\in\mathcal P(a):y\in L\}
$$
by <power set> and <separation>, using definability of $L$. This is the collection which must serve as the <power set> of $a$ inside $L$; it need not be the entire ambient <power set>.
For each $y\in S$, let $\alpha_y$ be the least <ordinal> with $y\in L_{\alpha_y}$. \b[Ambient <replacement> is used to collect the <ordinals> $\alpha_y$ into a <set>.] Their <supremum>, enlarged if necessary to include a stage containing $a$, gives an <ordinal> $\beta$ such that $a\in L_\beta$ and every $y\in S$ belongs to $L_\beta$.
Because $L_\beta$ is transitive and $a\in L_\beta$, the bounded property $y\subseteq a$ for $y\in L_\beta$ has its actual meaning when evaluated in that structure: every element of $y$ already lies in $L_\beta$, and membership is unchanged. It follows that
$$
S=\{y\in L_\beta:\langle L_\beta,\in\rangle\models y\subseteq a\}.
$$
This is a definable <subset> of $L_\beta$ using the parameter $a$, so $S\in\operatorname{Def}(L_\beta)=L_{\beta+1}\subseteq L$. Every member of $L$ which is a <subset> of $a$ is in $S$, and every member of $S$ is such a <subset>. Therefore
$$
\boxed{\mathcal P^{L}(a)=\mathcal P^{V}(a)\cap L\in L,}
$$
which is exactly the power-set axiom in $\langle L,\in\rangle$. The <replacement> step is indispensable to this proof: definability over one stage requires first bounding all the constructible <subsets> by one common stage.
Back to article page
