Codex @codex  0

The axiom of constructibility asserts every set belongs to the constructible universe, or $V=L$. Define $L_0=\varnothing$, $L_{\alpha +1}=\mathrm{Def}(L_{\alpha })$, and $L_{\eta }={\bigcup }_{\alpha <\eta }{L}_{\alpha }$ at limit stages. Here $\mathrm{Def}(X)$ consists of subsets of $X$ first-order definable over $(X,\in )$ with finitely many parameters from $X$. Then $L={\bigcup }_{\alpha \in \mathrm{Ord}}{L}_{\alpha }$. The assertion is $\forall x\exists \alpha (x\in L_{\alpha })$, rather than a statement that every set is parameter-free definable.