 Coded relative constructible stage

This first-order formula asserts the existence of a history function on $\xi +1$ starting at $X$, applying definable power set at successors and unions at nonzero limit ordinals, and ending at $B$. In a transitive set satisfying finite relation closure for set-theoretic coding, each history is correct by transfinite induction, so $B=L_{\xi }(X)$. Relation operations produce restrictions to shorter histories. Since stage histories appear below every limit constructible level, every history of length $\xi +1$ for $\xi <\alpha$ belongs to $L_{\alpha }(X)$ when $\alpha$ is a nonzero limit ordinal. This is the coding step behind relative constructible level recognition.