Definition 19: Let x and y be variables. We recursively define when x is said to be freely substitutable for y in a statement:
(a) Base cases: x is freely substitutable for y in a membership statement.
(b) Base cases: If x does not occur free in \phi , then x is freely substitutable for y in the existence statement \exists y \phi .
(c) Recursion: If x is freely substitutable for y in both of \phi and \psi , then so is it in the conjunction (\phi \wedge \psi) .
(d) Recursion: If x is freely substitutable for y in \phi , then so is it in the negation \neg \phi .
(e) Recursion: For a variable z distinct from y , if x is freely substitutable for y in \phi , then so is it in the existence statement \exists z \phi .