The variables of a term exist and are unique

Proof

1. 1
   By strong induction on : assume every term of length has existing uniquely (the induction hypothesis, "IH"); show the same for of length .
2. 2
   By T32 (ii), is either for a unique , or for a unique - never both.
3. 3
   Variable case. If : the var clause of D092 forces , a specific set (Pairing); by mutual exclusivity the func clause imposes no competing constraint, and by uniqueness of (T32 (ii)) this is the only set consistent with the var clause. Existence and uniqueness hold.
4. 4
   Function case, length bound. If with unique and : each for , by the same length bookkeeping as in the proof of T31.
5. 5
   By the IH, exists uniquely for every , so is a genuine function (D018), its image is a set (Replacement), and is a specific set (Union). The func clause of D092 then forces to equal it; by mutual exclusivity and uniqueness of , this is the only set consistent with D092.
6. 6
   T08 concludes: exists and is unique for every .

Used by