Isomorphisms preserve satisfaction

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

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)

An $L$-structure $\mathcal{M}$ has a nonempty set carrier $M$, values $c^{\mathcal{M}}\in M$, total functions $f^{\mathcal{M}}:M^{a(f)}\to M$, and relations $R^{\mathcal{M}}\subseteq M^{a(R)}$, supplied as set-indexed interpretation data. Logical equality is literal equality on $M$. An assignment is a function $s:\omega \to M$, also written $s(v_i)=s(i)$. The update $s[x:=b]$ changes only the value at variable $x$ to $b\in M$. For structures in the same signature a homomorphism $h:M\to N$ preserves constants and function values and takes related tuples to related tuples. It is strong if it also reflects every nonlogical relation. An embedding is an injective strong homomorphism; an isomorphism is a surjective embedding. A substructure has a nonempty subcarrier containing all constants, closed under all functions, with functions and relations restricted from the larger structure. A reduct keeps the carrier and only the interpretations for a smaller signature; an expansion is the reverse relationship. All finite powers and the assignment set $M^{\omega }$ are sets. Conventions and prerequisites: def-set-signature-and-finite-syntax-strings. (Structures and variable assignments)