[proofplan]
We compare the external constructible hierarchy $(L_\alpha)_{\alpha \in \operatorname{Ord}}$ with the hierarchy computed internally by the structure $(L,\in)$. The key point is that $L$ contains exactly the ambient ordinals and is transitive, so the stages available inside $L$ have the same ordinal indices. We then prove by transfinite induction that for every ordinal $\alpha$, the internal level $L_\alpha^{(L)}$ equals the external level $L_\alpha$. Since every element of $L$ belongs to some external $L_\alpha$, it therefore belongs to the same internal level, which is precisely the assertion that $(L,\in)$ satisfies $V=L$.
[/proofplan]
[step:Define the two constructible hierarchies to be compared]
Let $\operatorname{Ord}$ denote the class of ordinals in the ambient universe. The external constructible hierarchy is the class-indexed sequence $(L_\alpha)_{\alpha \in \operatorname{Ord}}$ defined by
\begin{align*}
L_0 &= \varnothing,\\
L_{\alpha+1} &= \operatorname{Def}(L_\alpha),\\
L_\lambda &= \bigcup_{\beta \in \lambda} L_\beta \quad \text{for every limit ordinal } \lambda,
\end{align*}
where $\operatorname{Def}(A)$ denotes the set of all subsets of $A$ that are first-order definable over the structure $(A,\in)$ with parameters from $A$. The constructible universe is
\begin{align*}
L = \bigcup_{\alpha \in \operatorname{Ord}} L_\alpha.
\end{align*}
Inside the structure $(L,\in)$, let $(L_\alpha^{(L)})_{\alpha \in \operatorname{Ord}^{(L)}}$ denote the constructible hierarchy computed using the same recursive definition, but with ordinals and definability interpreted internally in $(L,\in)$.
[/step]
[step:Identify the ordinals of $L$ with the ambient ordinals]
The structure $(L,\in)$ has exactly the same ordinals as the ambient universe. First, every ambient ordinal belongs to $L$: this follows by transfinite induction from the definition of the hierarchy, since each ordinal $\alpha$ is a set of earlier ordinals and hence appears at a constructible stage after its elements have appeared. Thus $\operatorname{Ord} \subset L$.
Conversely, $L$ is transitive: if $x \in y$ and $y \in L$, then $x \in L$. Therefore any ordinal of $(L,\in)$ is a transitive set well-ordered by $\in$ in the ambient universe, and hence is an ambient ordinal. Thus
\begin{align*}
\operatorname{Ord}^{(L)} = \operatorname{Ord}.
\end{align*}
[guided]
We need the internal hierarchy $(L_\alpha^{(L)})$ and the external hierarchy $(L_\alpha)$ to be indexed by the same ordinals. There are two inclusions to check.
First, every ambient ordinal lies in $L$. The external hierarchy is cumulative, and the definition of $L$ is built so that [ordinals are constructible](/theorems/4851): once all earlier ordinals $\beta \in \alpha$ have appeared, the set $\alpha=\{\beta:\beta \in \alpha\}$ appears at a later constructible stage. Hence each ambient ordinal $\alpha$ is an element of $L$.
Second, no new ordinals appear inside $L$. Since $L$ is transitive, membership between elements of $L$ is the same membership relation as in the ambient universe. Therefore if $a \in L$ is an ordinal according to $(L,\in)$, then $a$ is transitive and well-ordered by $\in$ in the ambient universe as well. Hence $a$ is an ambient ordinal. Combining both directions gives
\begin{align*}
\operatorname{Ord}^{(L)} = \operatorname{Ord}.
\end{align*}
[/guided]
[/step]
[step:Prove that $L$ computes each constructible level correctly]
We prove by transfinite induction on $\alpha \in \operatorname{Ord}$ that
\begin{align*}
L_\alpha^{(L)} = L_\alpha.
\end{align*}
For $\alpha=0$, both definitions give
\begin{align*}
L_0^{(L)}=\varnothing=L_0.
\end{align*}
Assume $L_\alpha^{(L)}=L_\alpha$. Then
\begin{align*}
L_{\alpha+1}^{(L)}
&= \operatorname{Def}^{(L)}(L_\alpha^{(L)})\\
&= \operatorname{Def}^{(L)}(L_\alpha)\\
&= \operatorname{Def}(L_\alpha)\\
&= L_{\alpha+1}.
\end{align*}
The equality $\operatorname{Def}^{(L)}(L_\alpha)=\operatorname{Def}(L_\alpha)$ holds because definability over the set structure $(L_\alpha,\in)$ uses only quantifiers ranging over $L_\alpha$ and parameters from $L_\alpha$; the ambient structure containing $(L_\alpha,\in)$ does not change which subsets of $L_\alpha$ are first-order definable over that set structure.
Now let $\lambda$ be a limit ordinal, and assume $L_\beta^{(L)}=L_\beta$ for every $\beta \in \lambda$. Since $L$ and the ambient universe have the same ordinals, the internal predecessors of $\lambda$ are exactly the ordinals $\beta \in \lambda$. Therefore
\begin{align*}
L_\lambda^{(L)}
&= \bigcup_{\beta \in \lambda} L_\beta^{(L)}\\
&= \bigcup_{\beta \in \lambda} L_\beta\\
&= L_\lambda.
\end{align*}
By transfinite induction, $L_\alpha^{(L)}=L_\alpha$ for every ordinal $\alpha$.
[/step]
[step:Use the correct computation of levels to verify $V=L$ inside $L$]
Let $x \in L$. By the definition of $L$ as the union of the external constructible hierarchy, there exists an ambient ordinal $\alpha$ such that $x \in L_\alpha$. By the identification of ordinals, $\alpha$ is also an ordinal of $(L,\in)$. By the equality of internal and external levels proved above,
\begin{align*}
L_\alpha = L_\alpha^{(L)}.
\end{align*}
Hence
\begin{align*}
x \in L_\alpha^{(L)}.
\end{align*}
Thus $(L,\in)$ satisfies the sentence
\begin{align*}
\forall x\, \exists \alpha\,\bigl(\alpha \text{ is an ordinal} \wedge x \in L_\alpha\bigr),
\end{align*}
where $L_\alpha$ is interpreted as the internally constructed $\alpha$-th level. This is exactly the axiom of constructibility $V=L$ in the structure $(L,\in)$.
[/step]
