The constructible hierarchy and constructible rank

In ZF define

$L_0=\mathrm{\varnothing },L_{\alpha +1}=\mathrm{Def}(L_{\alpha }),L_{\lambda }={\bigcup }_{\beta <\lambda }{L}_{\beta }(\lambda \text{ a nonzero limit})\mathrm{.}$

The operation Def is Definable subsets of a membership structure. For each ordinal $\theta$, apply Transfinite recursion on $\theta +1$: an empty history gives the empty set, a successor-length history gives Def of its last value, and a nonzero limit-length history gives the union of its range. Each operation returns a unique set. Uniqueness on the shorter interval proves agreement of any two histories on their overlap. Thus $L_{\alpha }$ is uniformly definable from $\alpha$, independently of the interval chosen. Replacement supplies the set of earlier levels at a limit. No choice is used.

Write $x\in L$ for $\mathrm{\exists }\alpha \in \mathrm{Ord}(x\in L_{\alpha })$. This defines a class, not a set union over all ordinals. For $x\in L$, the first stage containing $x$ is neither zero nor a limit (a member of a union already occurs in a summand). It is uniquely $\alpha +1$. Define the constructible rank ${\rho }_L(x)=\alpha$. This is a partial definable class function with domain $L$.