Relativization agrees with induced set satisfaction

Given: Work in ZF unless the statement explicitly weakens or supplements it; fix the objects and hypotheses of the statement.

Fix a pure membership formula $\delta (z,\vec{p})$ defining a class $C=\{z:\delta (z,\vec{p})\}$. This is eliminable notation for a predicate, not a class object. For a fixed pure membership formula $\varphi$, first rename its binders away from the parameter variables $\vec{p}$. Define ${\varphi }^C$ by keeping atoms, commuting with Boolean constructors, and setting $(\mathrm{\exists }x\psi {)}^C=\mathrm{\exists }x(\delta (x,\vec{p})\wedge {\psi }^C),(\mathrm{\forall }x\psi {)}^C=\mathrm{\forall }x(\delta (x,\vec{p})\to {\psi }^C)\mathrm{.}$ Copies of $\delta (x,\vec{p})$ are inserted by capture-avoiding substitution and fresh internal bound variables. In the set case $C=M$ use the predicate $z\in M$, with a fresh parameter variable for $M$. This operation is meaningful even for an empty class. It does not make the empty class an admitted structure: carriers of structures remain nonempty. For proper classes, evaluation of ${\varphi }^C$ means a separate ambient formula for each fixed $\varphi$, not a uniform universe satisfaction relation. Conventions and prerequisites: prop-capture-avoiding-substitution. (Relativization to sets and definable classes)

For every set signature $L$ and $L$-structure $\mathcal{M}$ there is a unique set ${\mathrm{Sat}}_{\mathcal{M}}\subseteq {\mathrm{Form}}_L\times M^{\omega }$. Writing $\mathcal{M},s\models \varphi$ for membership, its clauses are $\mathcal{M},s\models u=v⟺\mathrm{⟦}u{\mathrm{⟧}}_s=\mathrm{⟦}v{\mathrm{⟧}}_s,$ $\mathcal{M},s\models R(t_1,\dots ,t_n)⟺(\mathrm{⟦}{t}_1{\mathrm{⟧}}_s,\dots ,\mathrm{⟦}{t}_n{\mathrm{⟧}}_s)\in R^{\mathcal{M}},$ $\mathcal{M},s\models \mathrm{\neg }\varphi ⟺\text{not }\mathcal{M},s\models \varphi ,$ $\mathcal{M},s\models \varphi \wedge \psi ⟺(\mathcal{M},s\models \varphi \text{ and }\mathcal{M},s\models \psi ),$ $\mathcal{M},s\models \mathrm{\exists }x\varphi ⟺\mathrm{\exists }b\in M(\mathcal{M},s[x:=b]\models \varphi )\mathrm{.}$ The set is uniformly first-order definable from $L$ and the structure data. (Existence and uniqueness of set satisfaction)