Lemma 47: Given a statement \phi and distinct variables x and y , the variable x occurs quantified in \phi precisely if it occurs in the variable substitution [\phi | x \to y].

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

Base cases: In this case, \phi is a membership statement. By the definition of quantified occurrence, no variable can then occur quantified in \phi . By the base cases in the definition of variable substitution, since y is distinct from x , the latter does not occur in any of the possibilities for [\phi|x \to y] , either.

Inductive step: There are three rules to check: (b), (c) and (d).

(b): Suppose \phi is a conjunction (\psi \wedge \xi) , and take as the induction hypothesis that the desired result is already known for \psi and for \xi . We know by definition that x occurs quantified in \phi precisely if it occurs quantified in at least one of \psi and \xi ; by the induction hypothesis, this is the case precisely if x occurs in at least one of [\psi|x \to y] and [\xi|x \to y] . But this is again the case (by definition of occurrence) precisely if x occurs in \big( [\psi | x \to y] \wedge [\xi | x \to y]\big), which is the definition of [\phi|x \to y].

(c): Suppose \phi is a negation \neg \psi , where the desired result is known for \psi . Then, similarly to above, we find that x occurs quantified in \phi precisely if it does in \psi , hence precisely if it occurs in [\psi| x \to y] , i.e. precisely if it occurs in \neg [\psi | x \to y], which is the definition of [\phi|x \to y] .

(d): Suppose \phi is an existence statement \exist z \psi for some variable z , and that the desired result is known for \psi . If z is identical to x , then x occurs quantified in \phi by definition. Also, [\phi|x \to y] is then just \phi , so x occurs in the latter since it occurs in the former (by definition of occurrence).

Suppose now that z is distinct from x . Similarly to the other cases, it follows that x occurs quantified in \phi precisely if it does in \psi , hence precisely if it occurs in [\psi| x \to y] , i.e. precisely if it occurs in \exist z [\psi | x \to y], which is the definition of [\phi|x \to y] . \square