Proposition/definition 22: We recursively define the variable substitution [\phi | x \to y], where \phi is a statement and x and y are variables. Recall the usual notation for membership, conjunction, negation and existential quantification. In the below, z and w are arbitrary variables distinct from x .
(a) Base cases: [(x \in x)|x \to y] is given by (y \in y) .
(b) Base cases: [(x \in z)|x \to y] is given by (y \in z) .
(c) Base cases: [(z \in x)|x \to y] is given by (z \in y) .
(d) Base cases: [(z \in w)|x \to y] is given by (z \in w) .
(e) Base cases: Given any statement \phi , [\exists x \phi | x \to y] \hspace{3mm} \textup{is given by} \hspace{3mm} \exists x \phi. (f) Recursion: If [\phi | x \to y] and [\psi | x \to y] are already known, then [(\phi \wedge \psi)| x \to y] \hspace{3mm} \textup{is given by} \hspace{3mm} \big( [\phi | x \to y] \wedge [\psi | x \to y] \big). (g) Recursion: If [\phi | x \to y] is already known, then [\neg \phi | x \to y] \hspace{3mm} \textup{is given by} \hspace{3mm} \neg [\phi | x \to y]. (h) Recursion: If [\phi | x \to y] is already known, then [\exists z \phi | x \to y] \hspace{3mm} \textup{is given by} \hspace{3mm} \exists z [\phi | x \to y].
It follows that [\phi | x \to y] is defined for every \phi and arbitrary x and y .

Proof: We will argue by structural induction over the recursive specification of statements. Suppose first that \phi is a membership statement, i.e. (u \in v) for some variables u and v . As any variable is either identical to x or distinct from x , the following cases are exhaustive:
(i) u and v are both identical to x .
(ii) u is identical to x while v is distinct from x .
(iii) u is distinct from x while v is identical to x .
(iv) u and v are both distinct from x .

Case (i) is covered by (a) above, while case (ii) is covered by (b), case (iii) is covered by (c), and case (iv) is covered by (d). This covers the base cases, i.e. (a), in the recursive specification of statements.

For recursion rule (b) in the specification of statements, suppose [\phi | x \to y] and [\psi | x \to y] are already known. This case is covered by (f) in the above. Similarly, (c) in the specification is covered by (g) above.

Finally, we consider recursion rule (d) in the specification. We need to show that [\exists u \phi | x \to y] is defined for any variable y . If u is identical to x , then this is covered by (e) above. Otherwise, this is covered by (h) above. \square