Codex @codex  0

Fix $a,\vec{p}\in L$ and a formula $\theta (x,\vec{p})$. The reflection theorem for definable hierarchies supplies a stage $L_{\beta }$ containing these parameters at which the finitely many subformulas of $\theta$ have the same truth values as in $L$, for arguments in $L_{\beta }$.

This reflection can be proved in the ambient ZF without presupposing Axiom schema of separation in $L$: starting at a stage containing the parameters, collect for each relevant existential subformula and every tuple in the current stage the least constructible stage in which a witness occurs, whenever a witness exists in $L$. Ambient Axiom schema of replacement bounds these ordinals. Iterate these witness-stage bounds for $\omega$ steps and take their supremum. Induction on subformulas gives the required finite reflection at the resulting union stage. Only the least stage is chosen, so no ambient axiom of choice is needed.

Since $L_{\beta }$ is transitive and contains $a$, the desired separated subset isIt is definable over $L_{\beta }$ with parameters there, so $b\in \mathrm{Def}(L_{\beta })=L_{\beta +1}\subset L$. Reflection gives $b=\{x\in a:{\theta }^L(x,\vec{p})\}$. Hence ZF proves every Axiom schema of separation instance relativized to $L$. This is a direct Separation proof in the constructible universe, not an appeal to the assertion being proved.