[proofplan] We prove first that the value of a term depends only on the variables occurring in that term. The formula statement is then proved by structural induction on $\varphi$. Atomic formulas reduce to the term lemma, Boolean connectives are handled by the induction hypothesis, and quantifiers are handled by comparing the modified assignments $s[x \mapsto a]$ and $s'[x \mapsto a]$ after the bound variable is assigned the same element $a \in |M|$. [/proofplan] [step:Prove that term values depend only on the variables occurring in the term] Let $\operatorname{Var}(t)$ denote the set of variables occurring in an $L$-term $t$, and let $t^M[s] \in |M|$ denote the interpretation of $t$ in $M$ under an assignment $s: \operatorname{Var}_L \to |M|$. [claim:Term dependence on occurring variables] For every $L$-term $t$ and all assignments $s,s': \operatorname{Var}_L \to |M|$, if $s(y)=s'(y)$ for every $y \in \operatorname{Var}(t)$, then \begin{align*} t^M[s] = t^M[s']. \end{align*} [/claim] [proof] We prove the claim by structural induction on the term $t$. If $t$ is a variable $y$, then $\operatorname{Var}(t)=\{y\}$ and $t^M[s]=s(y)$, while $t^M[s']=s'(y)$. The hypothesis gives $s(y)=s'(y)$, hence $t^M[s]=t^M[s']$. Now suppose $t$ has the form $f(t_1,\dots,t_n)$, where $f$ is an $n$-ary function symbol of $L$ and $t_1,\dots,t_n$ are $L$-terms. Let \begin{align*} f^M: |M|^n \to |M| \end{align*} be the interpretation of $f$ in $M$. By definition, \begin{align*} \operatorname{Var}(t)=\bigcup_{i=1}^{n}\operatorname{Var}(t_i). \end{align*} If $s$ and $s'$ agree on $\operatorname{Var}(t)$, then they agree on $\operatorname{Var}(t_i)$ for each $i \in \{1,\dots,n\}$. By the induction hypothesis applied to each $t_i$, \begin{align*} t_i^M[s] = t_i^M[s'] \end{align*} for every $i \in \{1,\dots,n\}$. Therefore \begin{align*} t^M[s] &= f^M(t_1^M[s],\dots,t_n^M[s]) \\ &= f^M(t_1^M[s'],\dots,t_n^M[s']) \\ &= t^M[s']. \end{align*} This completes the induction on terms. [/proof] [/step] [step:Handle atomic formulas using the term dependence lemma] We begin the structural induction on the formula $\varphi$. Suppose first that $\varphi$ is an equality formula $t_1=t_2$. Then \begin{align*} \operatorname{FV}(\varphi)=\operatorname{Var}(t_1)\cup \operatorname{Var}(t_2). \end{align*} If $s$ and $s'$ agree on $\operatorname{FV}(\varphi)$, then they agree on each $\operatorname{Var}(t_i)$. By the term dependence claim, \begin{align*} t_i^M[s]=t_i^M[s'] \end{align*} for $i=1,2$. Hence \begin{align*} M \models t_1=t_2[s] &\iff t_1^M[s]=t_2^M[s] \\ &\iff t_1^M[s']=t_2^M[s'] \\ &\iff M \models t_1=t_2[s']. \end{align*} Now suppose $\varphi$ is an atomic relation formula $R(t_1,\dots,t_n)$, where $R$ is an $n$-ary relation symbol of $L$. Let \begin{align*} R^M \subset |M|^n \end{align*} be the interpretation of $R$ in $M$. Since \begin{align*} \operatorname{FV}(\varphi)=\bigcup_{i=1}^{n}\operatorname{Var}(t_i), \end{align*} agreement of $s$ and $s'$ on $\operatorname{FV}(\varphi)$ implies, by the term dependence claim, that \begin{align*} t_i^M[s]=t_i^M[s'] \end{align*} for every $i \in \{1,\dots,n\}$. Therefore \begin{align*} M \models R(t_1,\dots,t_n)[s] &\iff (t_1^M[s],\dots,t_n^M[s]) \in R^M \\ &\iff (t_1^M[s'],\dots,t_n^M[s']) \in R^M \\ &\iff M \models R(t_1,\dots,t_n)[s']. \end{align*} [/step] [step:Pass the dependence statement through Boolean connectives] Assume the theorem has been proved for formulas $\psi$ and $\theta$. For negation, let $\varphi$ be $\neg \psi$. Then $\operatorname{FV}(\varphi)=\operatorname{FV}(\psi)$. If $s$ and $s'$ agree on $\operatorname{FV}(\varphi)$, then they agree on $\operatorname{FV}(\psi)$, so the induction hypothesis gives \begin{align*} M \models \psi[s] \iff M \models \psi[s']. \end{align*} Using the semantic clause for negation, \begin{align*} M \models \neg\psi[s] &\iff \text{not } M \models \psi[s] \\ &\iff \text{not } M \models \psi[s'] \\ &\iff M \models \neg\psi[s']. \end{align*} For conjunction, let $\varphi$ be $\psi \land \theta$. Then \begin{align*} \operatorname{FV}(\varphi)=\operatorname{FV}(\psi)\cup \operatorname{FV}(\theta). \end{align*} If $s$ and $s'$ agree on $\operatorname{FV}(\varphi)$, then they agree on both $\operatorname{FV}(\psi)$ and $\operatorname{FV}(\theta)$. By the induction hypothesis, \begin{align*} M \models \psi[s] &\iff M \models \psi[s'], \\ M \models \theta[s] &\iff M \models \theta[s']. \end{align*} Thus \begin{align*} M \models (\psi \land \theta)[s] &\iff \bigl(M \models \psi[s]\text{ and }M \models \theta[s]\bigr) \\ &\iff \bigl(M \models \psi[s']\text{ and }M \models \theta[s']\bigr) \\ &\iff M \models (\psi \land \theta)[s']. \end{align*} Other Boolean connectives are handled either by their corresponding semantic clauses or as abbreviations in terms of $\neg$ and $\land$. [/step] [step:Compare modified assignments for existential quantifiers] Assume the theorem has been proved for a formula $\psi$, and let $\varphi$ be $\exists x\,\psi$. Let $a \in |M|$, and define the modified assignments \begin{align*} s[x \mapsto a]: \operatorname{Var}_L &\to |M|, \\ y &\mapsto \begin{cases} a, & y=x,\\ s(y), & y\ne x, \end{cases} \end{align*} and \begin{align*} s'[x \mapsto a]: \operatorname{Var}_L &\to |M|, \\ y &\mapsto \begin{cases} a, & y=x,\\ s'(y), & y\ne x. \end{cases} \end{align*} Since \begin{align*} \operatorname{FV}(\exists x\,\psi)=\operatorname{FV}(\psi)\setminus\{x\}, \end{align*} agreement of $s$ and $s'$ on $\operatorname{FV}(\exists x\,\psi)$ implies that, for every $a \in |M|$, the assignments $s[x\mapsto a]$ and $s'[x\mapsto a]$ agree on $\operatorname{FV}(\psi)$. Indeed, if $y=x$, both modified assignments send $y$ to $a$; if $y\ne x$ and $y \in \operatorname{FV}(\psi)$, then $y \in \operatorname{FV}(\exists x\,\psi)$, so $s(y)=s'(y)$. By the induction hypothesis applied to $\psi$, \begin{align*} M \models \psi[s[x\mapsto a]] \iff M \models \psi[s'[x\mapsto a]] \end{align*} for every $a \in |M|$. Therefore, using the semantic clause for the existential quantifier, \begin{align*} M \models \exists x\,\psi[s] &\iff \text{there exists }a \in |M|\text{ such that }M \models \psi[s[x\mapsto a]] \\ &\iff \text{there exists }a \in |M|\text{ such that }M \models \psi[s'[x\mapsto a]] \\ &\iff M \models \exists x\,\psi[s']. \end{align*} [guided] The point of the quantifier case is that the value assigned to the bound variable $x$ is overwritten. Fix an element $a \in |M|$, and define two assignments by changing only the value of $x$: \begin{align*} s[x \mapsto a]: \operatorname{Var}_L &\to |M|, \\ y &\mapsto \begin{cases} a, & y=x,\\ s(y), & y\ne x, \end{cases} \end{align*} and \begin{align*} s'[x \mapsto a]: \operatorname{Var}_L &\to |M|, \\ y &\mapsto \begin{cases} a, & y=x,\\ s'(y), & y\ne x. \end{cases} \end{align*} We must check that these two modified assignments agree on all free variables of $\psi$, because that is the hypothesis needed to apply the induction hypothesis to $\psi$. Let $y \in \operatorname{FV}(\psi)$. If $y=x$, then both modified assignments send $y$ to $a$. If $y\ne x$, then $y$ remains free after the quantifier is added, so \begin{align*} y \in \operatorname{FV}(\psi)\setminus\{x\} = \operatorname{FV}(\exists x\,\psi). \end{align*} By the hypothesis on $s$ and $s'$, this gives $s(y)=s'(y)$, and hence \begin{align*} s[x\mapsto a](y)=s'[x\mapsto a](y). \end{align*} Thus $s[x\mapsto a]$ and $s'[x\mapsto a]$ agree on $\operatorname{FV}(\psi)$. The induction hypothesis applied to $\psi$ now gives, for every $a \in |M|$, \begin{align*} M \models \psi[s[x\mapsto a]] \iff M \models \psi[s'[x\mapsto a]]. \end{align*} Using the semantic clause for the existential quantifier, we obtain \begin{align*} M \models \exists x\,\psi[s] &\iff \text{there exists }a \in |M|\text{ such that }M \models \psi[s[x\mapsto a]] \\ &\iff \text{there exists }a \in |M|\text{ such that }M \models \psi[s'[x\mapsto a]] \\ &\iff M \models \exists x\,\psi[s']. \end{align*} This proves the existential quantifier case. [/guided] [/step] [step:Handle universal quantifiers and complete the structural induction] Assume universal quantification is primitive, assume the theorem has been proved for $\psi$, and let $\varphi$ be $\forall x\,\psi$. Fix $a \in |M|$, and define the modified assignments $s[x \mapsto a]: \operatorname{Var}_L \to |M|$ and $s'[x \mapsto a]: \operatorname{Var}_L \to |M|$ as in the existential case: each sends $x$ to $a$, while $s[x \mapsto a]$ agrees with $s$ on every variable $y \ne x$ and $s'[x \mapsto a]$ agrees with $s'$ on every variable $y \ne x$. Since \begin{align*} \operatorname{FV}(\forall x\,\psi)=\operatorname{FV}(\psi)\setminus\{x\}, \end{align*} agreement of $s$ and $s'$ on $\operatorname{FV}(\forall x\,\psi)$ implies that $s[x\mapsto a]$ and $s'[x\mapsto a]$ agree on $\operatorname{FV}(\psi)$. Indeed, if $y=x$, then both modified assignments send $y$ to $a$. If $y\ne x$ and $y \in \operatorname{FV}(\psi)$, then $y \in \operatorname{FV}(\forall x\,\psi)$, so $s(y)=s'(y)$, and therefore $s[x\mapsto a](y)=s'[x\mapsto a](y)$. Hence, by the induction hypothesis applied to $\psi$, \begin{align*} M \models \psi[s[x\mapsto a]] \iff M \models \psi[s'[x\mapsto a]] \end{align*} for every $a \in |M|$. Using the semantic clause for the universal quantifier, \begin{align*} M \models \forall x\,\psi[s] &\iff \text{for every }a \in |M|,\ M \models \psi[s[x\mapsto a]] \\ &\iff \text{for every }a \in |M|,\ M \models \psi[s'[x\mapsto a]] \\ &\iff M \models \forall x\,\psi[s']. \end{align*} The atomic, Boolean, and quantifier cases exhaust the construction of first-order $L$-formulas. By structural induction, for every $L$-formula $\varphi$, satisfaction of $\varphi$ in $M$ under an assignment depends only on the values assigned to variables in $\operatorname{FV}(\varphi)$. Therefore, if $s(x)=s'(x)$ for every $x \in \operatorname{FV}(\varphi)$, then \begin{align*} M\models\varphi[s] \iff M\models\varphi[s']. \end{align*} [/step]