Lemma 27: Given a statement \phi in which some variable y does not occur, each variable x is freely substitutable for y in \phi .

Proof: We will argue by means of structural induction over the the recursive definition of occurrence of a variable in a statement.

Base cases: First, by the definition of free substitutability, x is always freely substitutable for y in any membership statement, including those in which y does not occur. This covers base cases (a) and (b) in the definition. Moreover, it is not possible for y not to occur in existence statements of the form \exists y \phi , so there is nothing to check for base case (c) in the definition.

Inductive step: Suppose that x is freely substitutable for y in two statements \phi and \psi in which y does not occur. Then, by definition of free substitutability, x is freely substitutable for y in the conjunction (\phi \wedge \psi) as well as in the negation \neg \phi . This covers recursion rules (d) and (e) of the definition.

Finally, given a variable z such that y does not occur in \exists z \phi , we must show that x is freely substitutable for y in \exists z \phi . But if y does not occur in \exists z \phi , then y must by definition of occurrence be distinct from z ; therefore, we get by definition of free substitutability that x is freely substitutable for y in \exists z \phi . This covers rule (f) of the definition of occurrence. \square