Theorem ax10 200

Description: Axiom of Quantifier Substitution. Appears as Lemma L12 in [Megill] p. 445 (p. 12 of the preprint).

Assertion

Ref	Expression
ax10	|- T. |= [(A.\x:al [x:al = y:al]) ==> (A.\y:al [y:al = x:al])]

Distinct variable group:   x,y,al

Proof of Theorem ax10

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		wv 58	. . . . . 6 |- z:al:al
2		wv 58	. . . . . . . 8 |- x:al:al
3		wv 58	. . . . . . . 8 |- y:al:al
4	2, 3	weqi 68	. . . . . . 7 |- [x:al = y:al]:*
5		weq 38	. . . . . . . 8 |- = :(al -> (al -> *))
6	5, 2, 1	wov 64	. . . . . . . . 9 |- [x:al = z:al]:*
7	6	id 25	. . . . . . . 8 |- [x:al = z:al] |= [x:al = z:al]
8	5, 2, 3, 7	oveq1 89	. . . . . . 7 |- [x:al = z:al] |= [[x:al = y:al] = [z:al = y:al]]
9	4, 1, 8	cla4v 142	. . . . . 6 |- (A.\x:al [x:al = y:al]) |= [z:al = y:al]
10	4	ax4 140	. . . . . . 7 |- (A.\x:al [x:al = y:al]) |= [x:al = y:al]
11	2, 10	eqcomi 70	. . . . . 6 |- (A.\x:al [x:al = y:al]) |= [y:al = x:al]
12	1, 9, 11	eqtri 85	. . . . 5 |- (A.\x:al [x:al = y:al]) |= [z:al = x:al]
13	12	alrimiv 141	. . . 4 |- (A.\x:al [x:al = y:al]) |= (A.\z:al [z:al = x:al])
14		wal 124	. . . . . 6 |- A.:((al -> *) -> *)
15	4	wl 59	. . . . . 6 |- \x:al [x:al = y:al]:(al -> *)
16	14, 15	wc 45	. . . . 5 |- (A.\x:al [x:al = y:al]):*
17	3, 2	weqi 68	. . . . . . 7 |- [y:al = x:al]:*
18	17	wl 59	. . . . . 6 |- \y:al [y:al = x:al]:(al -> *)
19	3, 1	weqi 68	. . . . . . . . 9 |- [y:al = z:al]:*
20	19	id 25	. . . . . . . 8 |- [y:al = z:al] |= [y:al = z:al]
21	5, 3, 2, 20	oveq1 89	. . . . . . 7 |- [y:al = z:al] |= [[y:al = x:al] = [z:al = x:al]]
22	17, 21	cbv 168	. . . . . 6 |- T. |= [\y:al [y:al = x:al] = \z:al [z:al = x:al]]
23	14, 18, 22	ceq2 80	. . . . 5 |- T. |= [(A.\y:al [y:al = x:al]) = (A.\z:al [z:al = x:al])]
24	16, 23	a1i 28	. . . 4 |- (A.\x:al [x:al = y:al]) |= [(A.\y:al [y:al = x:al]) = (A.\z:al [z:al = x:al])]
25	13, 24	mpbir 77	. . 3 |- (A.\x:al [x:al = y:al]) |= (A.\y:al [y:al = x:al])
26		wtru 40	. . 3 |- T.:*
27	25, 26	adantl 51	. 2 |- (T., (A.\x:al [x:al = y:al])) |= (A.\y:al [y:al = x:al])
28	27	ex 148	1 |- T. |= [(A.\x:al [x:al = y:al]) ==> (A.\y:al [y:al = x:al])]

Syntax hints:  tv 1   -> ht 2  *hb 3  kc 5  \kl 6   = ke 7  T.kt 8  [kbr 9   |= wffMMJ2 11   ==> tim 111  A.tal 112

This theorem was proved from axioms:  ax-syl 15  ax-jca 17  ax-simpl 20  ax-simpr 21  ax-id 24  ax-trud 26  ax-cb1 29  ax-cb2 30  ax-refl 39  ax-eqmp 42  ax-ded 43  ax-ceq 46  ax-beta 60  ax-distrc 61  ax-leq 62  ax-distrl 63  ax-hbl1 93  ax-17 95  ax-inst 103  ax-eta 165

This theorem depends on definitions:  df-ov 65  df-al 116  df-an 118  df-im 119

This theorem is referenced by: (None)