Solution (source code)

= Solution

A <standard membership model of set theory> has the actual membership relation:
$$
\boxed{E^M=\in\upharpoonright(M\times M),\qquad (M,\in)\models\mathrm{ZFC}.}
$$
When “standard model” is used with the transitive-model convention, one also requires $M$ to be transitive: $x\in y\in M$ implies $x\in M$. Under a convention where standard means only actual membership, this extra requirement defines a <transitive model>. The <set-theoretic absoluteness> arguments below use transitive models of <ZFC>, so that bounded quantification and <ordinals> have their intended meaning.