Solution (source code)

= Solution

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. Hence
$$
\boxed{\psi^M(\vec b)\leftrightarrow\psi^N(\vec b)\qquad\text{for every syntactic }\Delta_0\text{ formula and }\vec b\in M.}
$$
No <ZF> axioms are needed for this syntactic statement beyond the ambient meaning of a <transitive class>. For a <ZF-equivalent bounded formula> $\varphi$, choose a bounded equivalent $\psi$. The assumption that both structures model <ZF> gives $\varphi^M\leftrightarrow\psi^M$ and $\varphi^N\leftrightarrow\psi^N$. Combining these with the displayed equivalence proves the asserted <set-theoretic absoluteness> of $\Delta_0^{\mathrm{ZF}}$.