 Solution

Fix $a\in L$. In the ambient universe form the setby 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}$. 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 thatThis is a definable subset of $L_{\beta }$ using the parameter $a$, so $S\in \mathrm{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. Thereforewhich is exactly the power-set axiom in $⟨L,\in ⟩$. The replacement step is indispensable to this proof: definability over one stage requires first bounding all the constructible subsets by one common stage.