The free variables of a formula exist and are unique

Proof

1. 1
   By strong induction on : assume every formula of length has existing uniquely (the induction hypothesis, "IH"); show the same for of length .
2. 2
   By T35 (ii), is exactly one of the five forms of D083.
3. 3
   eq, rel. If ( ): T37 gives and exist uniquely, so their union (D004) is a specific set; the eq clause of D093 forces to equal it. Similarly if : is a genuine function (by T37), its image is a set (Replacement), and of that image is a specific set (Union); the rel clause forces to equal it.
4. 4
   neg. If ( , as in the proof of T36): by the IH, exists uniquely; the neg clause of D093 forces .
5. 5
   bin. If ( , as in the proof of T36): by the IH, and exist uniquely, so their union is a specific set; the bin clause forces to equal it.
6. 6
   quant. If ( , ): by the IH, exists uniquely, so (Separation) is a specific set; the quant clause forces to equal it.
7. 7
   In every case, mutual exclusivity of the five forms (T35 (ii)) and uniqueness of each form's witnesses leave exactly one set consistent with D093. T08 concludes: exists and is unique for every .

Used by