**Description: **Axiom ax-11o 1720 ("o" for "old") was the
original version of ax-11 1413,
before it was discovered (in Jan. 2007) that the shorter ax-11 1413 could
replace it. It appears as Axiom scheme C15' in [Megill] p. 448 (p. 16 of
the preprint). It is based on Lemma 16 of [Tarski] p. 70 and Axiom C8 of
[Monk2] p. 105, from which it can be proved
by cases. To understand this
theorem more easily, think of "¬ ∀𝑥𝑥 = 𝑦 →..." as informally
meaning "if 𝑥 and 𝑦 are distinct variables
then..." The
antecedent becomes false if the same variable is substituted for 𝑥 and
𝑦, ensuring the theorem is sound
whenever this is the case. In some
later theorems, we call an antecedent of the form ¬
∀𝑥𝑥 = 𝑦 a
"distinctor."
This axiom is redundant, as shown by theorem ax11o 1719.
This axiom is obsolete and should no longer be used. It is proved above
as theorem ax11o 1719. (Contributed by NM, 5-Aug-1993.)
(New usage is discouraged.) |