Proposition 42: Let a, b, ..., z as well as \mathtt{u} and \mathtt{v} be variables, and \phi a statement. Recall the usual notation for iterated existence statements.
(a) If \mathtt{u} is among a, b, ..., z , the variable substitution [\exist a, b, ..., z \phi | \mathtt{u} \to \mathtt{v}] is given by \exist a, b, ..., z \phi .
(b) If \mathtt{u} is not among a, b, ..., z , then [\exist a, b, ..., z \phi | \mathtt{u} \to \mathtt{v}] is given by \exist a, b, ..., z [\phi | \mathtt{u} \to \mathtt{v}].
Proof: (a): We will use structural induction over the definition of iterated existence statements.
Base cases: Suppose \mathtt{u} is among the variables a and b . By definition, we know that \exists a, b is shorthand for \exists a \exists b \phi . There are at most two possibilities: \mathtt{v} is identical to a , or \mathtt{v} is identical to b (these coincide if a is identical to b ). Supposing the former, (e) in the definition of variable substitution tells us [\exists a \exists b | \mathtt{u} \to \mathtt{v}] is defined as \exists a \exists b \phi , i.e. as \exists a, b \phi . Thus, we are done in this case.
Suppose now that \mathtt{v} is identical to b but distinct from a . Then, by (h) in the definition of variable substitution, [\exists a \exists b \phi | \mathtt{u} \to \mathtt{v}] is given by \exists a [ \exists b \phi | \mathtt{u} \to \mathtt{v}]. But [ \exists b \phi | \mathtt{u} \to \mathtt{v}] is now given by \exists b \phi , using (e) in the definition of variable substitution. Therefore, [\exists a \exists b \phi | \mathtt{u} \to \mathtt{v}] is again given by \exist a \exists b \phi , i.e. \exists a, b \phi .
Inductive step: We take as the induction hypothesis that for the variables b, c, ..., z , we know that [\exist b, c, ..., z | \mathtt{u} \to \mathtt{v}] is given by \exist b, c, ..., z \phi whenever \mathtt{u} is among b, c, ..., z . Suppose now that \mathtt{u} is among the variables a, b, c, ..., z . If \mathtt{u} is identical to a , then we get by (e) in the definition of variable substitution that [\exists a, b, c, ..., z \phi | \mathtt{u} \to \mathtt{v}] is given by \exists a, b, c, ..., z \phi , as \exists a, b, c, ..., z is shorthand for \exists a \exists b, c, ..., z \phi .
On the other hand, if \mathtt{u} is not identical to a , then it must instead be among the variables b, c, ..., z . By (h) in the definition of variable substitution we then know [\exists a, b, c, ..., z \phi | \mathtt{u} \to \mathtt{v}] is given by \exists a [\exists b, c, ..., z \phi | \mathtt{u} \to \mathtt{v}]. By the induction hypothesis, we know that this is the same as \exists a \exists b, c, ..., z \phi , which is the defnition of \exists a, b, c, ..., z \phi .
(b): We again use structural induction, over the same definition as above.
Base cases: Suppose \mathtt{u} is distinct from both a and b . Since \exists a, b \phi is short for \exists a \exists b \phi , (h) in the definition of variable substitution tells us [\exists a, b \phi | \mathtt{u} \to \mathtt{v}] is \exists a [\exists b \phi | \mathtt{u} \to \mathtt{v}]. Using the same part of the definition again, this is the same as \exists a \exists b [\phi | \mathtt{u} \to \mathtt{v}]. Inductive step: We take as the induction hypothesis that for the variables b, c, ..., z , we have that [\exist b, c, ..., z | \mathtt{u} \to \mathtt{v}] is given by \exist b, c, ..., z [\phi | \mathtt{u} \to \mathtt{v}] whenever \mathtt{u} is not among b, c, ..., z . Suppose now that \mathtt{u} is not among the variables a, b, c, ..., z . As \exists a, b, c, ..., z \phi is short for \exists a \exists b, c, ..., z \phi , we get using (h) in the definition of variable substitution that [\exist a, b, c, ..., z \phi | \mathtt{u} \to \mathtt{v}] is given by \exists a [\exists b, c, ..., z \phi | \mathtt{u} \to \mathtt{v}], which by the induction hypothesis is the same as \exists a \exists b, c, ..., z [\phi | \mathtt{u} \to \mathtt{v}], i.e. the same as \exists a, b, c, ..., z [\phi | \mathtt{u} \to \mathtt{v}] . \square