Axiom ax-11o 1220

Description: Axiom ax-11o 1220 ("o" for "old") was the original version of ax-11 969, before it was discovered (in Jan. 2007) that the shorter ax-11 969 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 "-. A.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 -. A.xx = y a "distinctor."

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

Assertion

Ref	Expression
ax-11o	|- (-. A.x x = y -> (x = y -> (ph -> A.x(x = y -> ph))))

Detailed syntax breakdown of Axiom ax-11o

Step	Hyp	Ref	Expression
1		vx	. . . . . 6 set x
2	1	cv 957	. . . . 5 class x
3		vy	. . . . . 6 set y
4	3	cv 957	. . . . 5 class y
5	2, 4	wceq 958	. . . 4 wff x = y
6	5, 1	wal 956	. . 3 wff A.x x = y
7	6	wn 2	. 2 wff -. A.x x = y
8		wph	. . . 4 wff ph
9	5, 8	wi 3	. . . . 5 wff (x = y -> ph)
10	9, 1	wal 956	. . . 4 wff A.x(x = y -> ph)
11	8, 10	wi 3	. . 3 wff (ph -> A.x(x = y -> ph))
12	5, 11	wi 3	. 2 wff (x = y -> (ph -> A.x(x = y -> ph)))
13	7, 12	wi 3	1 wff (-. A.x x = y -> (x = y -> (ph -> A.x(x = y -> ph))))

This axiom is referenced by:  ax11 1221  ax11b 1222  equs5 1223  ax11v 1267  a12study 1380  a12studyALT 1381

Copyright terms: Public domain