Lemma 30: A variable x occurs in a statement \phi precisely if x occurs free in \phi or occurs quantified in \phi , or both.
Proof: We use structural induction over the specification of statements.
Base cases: Suppose \phi is a membership statement. The rules for whether x occurs in \phi or occurs free in \phi are then the same (these are given by various base cases in the definition of occurrence and of free occurrence). On the other hand, by definition, x cannot occur quantified in \phi , so this event is not relevant here, leaving the coincidence of occurrence and free occurrence only.
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 . By definition, we know x occurs in \phi precisely if it occurs in at least one of \psi and \xi . This is by the induction hypothesis the case precisely if x occurs free or occurs quantified, or both, in at least one of \psi and \xi . But if x occurs free in one of these, then by definition it occurs free in \phi . Similarly, if it occurs quantified in one of these, then it occurs quantified in \phi .
(c): Suppose \phi is a negation \neg \psi and that the desired result is known for \psi . Similarly to above, we know x occurs in \phi precisely if it occurs in \psi , again meaning that x occurs free or occurs quantified, or both, in \psi . This is again the case precisely if x occurs free or occurs quantified in \phi , or both.
(d): Suppose \phi is a 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 in \phi and also occurs quantified in \phi (and does not occur free in \phi ), and we are done.
Suppose now that z is distinct from x . Then we know x occurs in \phi precisely if it occurs in \psi . But this is, by the induction hypothesis, the case precisely if x occurs free or occurs quantified, or both, in \psi , which is again the case precisely if x occurs free or occurs quantified in \phi . \square