Axiom ax-11o 1216

Description: Axiom ax-11o 1216 ("o" for "old") was the original version of ax-11 965, before it was discovered (in Jan. 2007) that the shorter ax-11 965 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 "¬ ∀xx = y →..." as informally meaning "if x and y are distinct variables then..." The antecedent becomes false if the same variable is substituted for x and y, ensuring the theorem is sound whenever this is the case. In some later theorems, we call an antecedent of the form ¬ ∀xx = y a "distinctor."

This axiom is redundant, as shown by theorem ax11o 1215.

Assertion

Ref	Expression
ax-11o	⊢ (¬ ∀x x = y → (x = y → (φ → ∀x(x = y → φ))))

Detailed syntax breakdown of Axiom ax-11o

Step	Hyp	Ref	Expression
1		vx	. . . . . 6 set x
2	1	cv 953	. . . . 5 class x
3		vy	. . . . . 6 set y
4	3	cv 953	. . . . 5 class y
5	2, 4	wceq 954	. . . 4 wff x = y
6	5, 1	wal 952	. . 3 wff ∀x x = y
7	6	wn 2	. 2 wff ¬ ∀x x = y
8		wph	. . . 4 wff φ
9	5, 8	wi 3	. . . . 5 wff (x = y → φ)
10	9, 1	wal 952	. . . 4 wff ∀x(x = y → φ)
11	8, 10	wi 3	. . 3 wff (φ → ∀x(x = y → φ))
12	5, 11	wi 3	. 2 wff (x = y → (φ → ∀x(x = y → φ)))
13	7, 12	wi 3	1 wff (¬ ∀x x = y → (x = y → (φ → ∀x(x = y → φ))))

This axiom is referenced by:  ax11 1217  ax11b 1218  equs5 1219  ax11v 1263  a12study 1376  a12studyALT 1377

Copyright terms: Public domain