Lemma 48: Let \phi be a statement and x and y variables. If a variable v occurs in the variable substitution [\phi | x \to y] but does not occur in \phi , then v is identical to y .

Proof: We use structural induction over the specification of statements.

Base cases: If \phi is a membership statement, then there are four possibilities, corresponding, respectively, to the first four base cases in the definition of variable substitution:
(a) Only x occurs in \phi , i.e. \phi is given by (x \in x) . Here, [\phi|x \to y] is given by (y \in y) .
(b) \phi is given by (x \in z) for some variable z . Now, [\phi|x \to y] is (y \in z) .
(c) \phi is given by (z \in x) for some variable z . In this case, [\phi|x \to y] is given by (z \in y) .
(d) x does not occur in \phi . Then, [\phi | x \to y] is given by \phi .

We see that in every instance, the only variable that occurs in [\phi | x \to y] but not in \phi , if there is such a variable, is y .

Inductive step: We check each of the recursion rules in the specification.

(b): Suppose \phi is a conjunction (\psi \wedge \xi) , and take as the induction hypothesis that the desired result is known for \psi and for \xi . Suppose that v is a variable occuring in [\phi | x \to y] but not in \phi . By definition of variable substitution, we get that [\phi | x \to y] is given by \big( [\psi | x \to y] \wedge [\xi | x \to y] \big). Thus, by definition of occurrence, v must occur in at least one of [\psi | x \to y] and [\xi | x \to y] . Furthermore, since \phi is (\psi \wedge \xi) and v does not occur in, we know v cannot occur in \psi nor in \xi . But then, by the induction hypothesis, whichever one(s) of [\psi| x \to y] and [\xi | x \to y] it is that v occurs in, it must be the case that v is identical to y .

(c): Suppose \phi is a negation \neg \psi and that the desired result is known for \psi , and that v occurs in [\phi | x \to y] but not in \phi . Similarly to above, we find that [\phi | x \to y] is given by \neg [\psi | x \to y], meaning v must occur in [\psi| x \to y] , and that since v cannot occur in \psi , we get by the induction hypothesis that v is identical to y .

(d): Suppose \phi is an existence statement \exist z \psi for some variable z , that the desired result is known for \psi , and that v occurs in [\phi | x \to y] but not in \phi . We note that if z were to be identical to x , then [\phi | x \to y] would be given by \exists z \psi , i.e. by \phi ; it is absurd that v should both occur and not occur in \phi , so we conclude z must be distinct from x . Hence, [\phi | x \to y] is given by \exist z [\psi | x \to y]. Notice that if v were identical to z , then again v would occur in both \phi and [\phi|x \to y] , an absurdity. Thus v is distinct from z . This means v must occur in [\psi | x \to y] , by definition of occurrence. As v cannot occur in \psi (or else it would occur in \phi ), the induction hypothesis tells us v is identical to y . \square