Lemma 46: For a statement \phi and variables x and y , the variable substitution \big[ [\phi | x \to y] \big| x \to y \big] is the same as [\phi | x \to y] .

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

Base cases: Suppose \phi is a membership statement (u \in v) for variables u and v . There are four possibilities:
(i) u and v are both identical to x .
(ii) u is identical to x , while v is distinct from x .
(iii) u is distinct from x , while v is identical to x .
(iv) u and v are both distinct from x .

These correspond, in order, to the first four base cases in the definition of variable substitution. In case (i), [\phi| x \to y] is given by (y \in y), hence \big[ [\phi | x \to y] \big| x \to y \big] is given by \big[ (y \in y) \big| x \to y \big], which is also defined as (y \in y) , as desired. Similarly, in case (ii), the two variable substitutions are both given by (y \in v) . In case (iii), both are given by (u \in y) . Finally, in case (iv), both are given by (u \in v) .

Inductive step: There are three recursion 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 known for \psi and for \xi . Since [\phi | x \to y] is defined as \big( [\psi | x \to y] \wedge [\xi | x \to y] \big), it follows that \big[ [\phi | x \to y] \big| x \to y \big] is given by \Big[ \big( [\psi | x \to y] \wedge [\xi | x \to y] \big) \Big| x \to y \Big]. This is again the same as \Big( \big[ [\psi | x \to y] \big| x \to y \big] \wedge \big[ [\xi | x \to y] \big| x \to y \big] \Big). Using the induction hypothesis, this is the same as \big( [\psi | x \to y] \wedge [\xi | x \to y] \big), which is the definition of [(\psi \wedge \xi) | x \to y] , i.e. of [\phi|x \to y] .

(c): Suppose \phi is a negation \neg \psi , and that the desired result is known for \psi . Similarly to above, since [\phi | x \to y] is here defined as \neg [\psi | x \to y] , we get that \big[ [\phi | x \to y] \big| x \to y \big] is given by \big[ \neg [\psi | x \to y] \big| x \to y] \big], which is again \neg \big[ [\psi | x \to y] \big| x \to y] \big], this being (by the induction hypothesis) given by \neg [\psi | x \to y] , i.e. [\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 the definition of [\phi | x \to y] is \phi , hence \big[ [\phi | x \to y] \big| x \to y \big] is the same as [\phi | x \to y] .

Suppose now that z is distinct from x . The definition of [\phi | x \to y] is then \exist z [\psi | x \to y] . It follows that \big[ [\phi | x \to y] \big| x \to y \big] is given by \big[ \exist z [\psi | x \to y] \big| x \to y \big], which by definition is the same as \exist z \big[ [\psi | x \to y] \big| x \to y \big]. By the induction hypothesis, this is \exist z [\psi | x \to y] , i.e. [\phi | x \to y] . \square