Bounded formulas are absolute for transitive sets

For $a,b\in M$, equality and membership in either structure mean the actual relations $a=b$ and $a\in b$. Thus the atomic cases agree. The formula constructors admit induction, so it remains to show that agreement is preserved by each constructor.

If $\varphi$ and $\psi$ agree on all tuples in $M$, their conjunctions agree because both conjuncts have the same truth values. Their negations agree because a truth value is false in one structure exactly when it is false in the other.

Let $a,\bar{b}\in M$. A witness $c$ for $\mathrm{\exists }x\in a\varphi (x,\bar{b})$ in either structure is an actual member of $a$. Transitivity puts every such $c$ in $M$, hence also in $N$. The induction hypothesis at $(c,\bar{b})$ transfers the matrix in either direction, retaining the same witness. If $a=\mathrm{\varnothing }$, both existential statements are false. Universal bounded quantifiers follow by negation.

Constructor induction now gives the asserted equivalence for every bounded formula. For fixed class definitions the same induction is a finite metatheoretic induction on the chosen formula, with each quantifier relativized; it requires no class satisfaction set.