Lemma 45: For a statement \phi and a variable x , the variable substitution [\phi|x \to x] is given by \phi .

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

Base cases: Suppose \phi is a membership statement (u \in v) , where u and v are variables. There are four cases to consider:
(a) u and v are both identical to x .
(b) u is identical to x , while v is not.
(c) u is distinct from x , while v is not.
(d) u and v are both distinct from x .

These cases correspond, in order, to the first four base cases in the definition of variable substitution. In case (a), [\phi|x \to x] is (x \in x) , In case (b) we get (x \in v) , in case (c) we get (u \in x) , and in case (d) we get (u \in v) . In all four cases, these statements are the same as (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 already known for \psi and for \xi . Then, [\phi|x \to x] is, by definition of variable substitution, given by \big( [\psi | x \to x] \wedge [\xi | x \to x]. We get by the induction hypothesis that this is the same as (\psi \wedge \xi) , i.e. \phi .

(c): Suppose \phi is a negation \neg \psi , and that the desired result is already known for \psi . Similarly to above, we get that [\phi | x \to x] is given by \neg [\psi | x \to x], which is the same as \neg \psi , i.e. the same as \phi .

(d): Suppose \phi is a negation \exist z \psi for some variable z , and that the desired result is already known for \psi . If z is identical to x , then we get by the final base case in the definition of variable substitution that [\phi | x \to x] is given by \exist z \psi , i.e. \phi . Suppose now that z and x are distinct. Then, by the last recursion rule in the definition of variable substitution, [\phi| x \to x] is given by \exist z [\psi | x \to x], which by the induction hypothesis is the same as \exist z \psi , i.e. the same as \phi . \square