Definition 13: Let x be a variable. We recursively define when x occurs in a statement. In the below, y is an arbitrary variable.
(a) Base cases: x occurs in the membership statement (x \in y). (b) Base cases: x occurs in the membership statement (y \in x). (c) Base cases: For any statement \phi , x occurs in the existence statement \exists x \phi. (d) Recursion: If x occurs in \phi or in \psi , then it occurs in the conjunction (\phi \wedge \psi). (e) Recursion: If x occurs in \phi , then it occurs in the negation \neg \phi. (f) Recursion: If x occurs in \phi then it occurs in the existence statement \exists y \phi.