Substitution into a formula exists and is 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 ( ): T39 gives and exist uniquely - unconditionally, independent of this induction - so is a specific term (D075); the eq clause of D098 forces to equal it. Similarly if : is a genuine function (by T39 applied to each entry), so is a specific formula; the rel clause forces to equal it.
4. 4
   neg, bin. If ( , as in the proof of T36): by the IH, exists uniquely, so the neg clause forces . Likewise if ( , ): by the IH applied to and to , both and exist uniquely, and the bin clause forces the value.
5. 5
   quant. If ( , ): exactly one of or holds. If , the same clause of D098 forces outright - no induction needed. If , the diff clause applies instead: by the IH, exists uniquely, so the clause forces . The same and diff clauses never both apply (their hypotheses , are exclusive).
6. 6
   In every case, mutual exclusivity of the five forms (T35 (ii)), and (in the quant case) of versus , leave exactly one formula consistent with D098. T08 concludes: exists and is unique for every .