Proposition/definition 32: To a statement \phi and variables x and y , we shall associate a statement known as the substitution in \phi of x for y , recursively defined below. This will be called a variable substitution, and denoted [\phi | x \to y].In the below, z and w are arbitrary variables each distinct from x . Recall the notation for membership, conjunction, negation and existence statements.
(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 use structural induction over the specification of statements. The argument can be repeated for an arbitrary choice of variables.

Base cases: These are part (a) of the specification. Here, \phi is a membership statement, i.e. of the form (u \in v) for some variables u and v . Each variable is either identical to or distinct from x , so 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).

Inductive step: There are three different recursion rules to check. For rule (b) in the specification, suppose (as the induction hypothesis) that both of [\phi | x \to y] and [\psi | x \to y] are already known. This case is covered by (f) in the above. Similarly, rule (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