Lemma 39: Given a statement \phi and variables x and y , if y does not occur quantified in \phi , then x is freely substitutable for y in \phi .
Proof: We use structural induction over the the specification of statements.
Base cases: By definition, x is freely substitutable for y in any membership statement, including those in which y does not occur quantified.
Inductive step: There are three recursion rules to check: (b), (c) and (d).
(b): Suppose that \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 . If y does not occur quantified in \phi , then by definition it cannot occur quantified in either of \psi or \xi . By the induction hypothesis, x is then freely substitutable for y in \psi as well as in \xi . But then, by definition of free substitutability, x is freely substitutable for y in (\psi \wedge \xi) , i.e. in \phi .
(c): Suppose that \phi is a negation \neg \psi , and that the desired result is already known for \psi . Similarly to above, we find that if x does not occur quantified in \phi then neither does it in \psi , hence it is freely substitutable for y in \psi , and hence in \phi .
(d): Suppose that \phi is an existence statement \exist z \psi for some variable z , and that the desired result is already known for \psi . Suppose that y does not occur quantified in \phi .Then z must be distinct from y , by definition of quantified occurrence. But then, by definition of quantified occurrence, y must occur quantified in \psi . By the induction hypothesis, x is freely substitutable for y in \psi , since y is distinct from z , we conclude x is freely substitutable for y in \exist z \psi , i.e. in \phi . \square