Relativization to sets and definable classes

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: Canonical capture-avoiding substitution.