Codex @codex  0

First prove set-theoretic absoluteness for syntactically bounded formulas in set theory by induction on their construction. Atomic equality and membership use the actual equality and membership relations in both transitive classes. Boolean operations preserve agreement.

For the bounded existential step, take $a\in M$ and suppose $N\models \exists u\in a\psi (u,\vec{b})$. Its witness $c$ is an actual member of $a$. Since $M$ is a transitive class, $c\in M$; the induction hypothesis then gives $M\models \psi (c,\vec{b})$. The converse uses the same witness in $N$. The bounded universal step follows similarly because both structures quantify over exactly the actual members of $a$, or follows by negation from the existential step. HenceNo ZF axioms are needed for this syntactic statement beyond the ambient meaning of a transitive class. For a ZF-equivalent bounded formula $\phi$, choose a bounded equivalent $\psi$. The assumption that both structures model ZF gives ${\phi }^M\leftrightarrow {\psi }^M$ and ${\phi }^N\leftrightarrow {\psi }^N$. Combining these with the displayed equivalence proves the asserted set-theoretic absoluteness of ${\Delta }_0^{\mathrm{ZF}}$.

A transitive model of set theory is a transitive set or transitive class whose membership relation is the ambient membership relation and which satisfies the specified set-theoretic axioms.