Theorem ax10 213

Description: Axiom of Quantifier Substitution. Appears as Lemma L12 in [Megill] p. 445 (p. 12 of the preprint). (Contributed by Mario Carneiro, 10-Oct-2014.)

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 64	. . . . . 6 |- z:al:al
2		wv 64	. . . . . . . 8 |- x:al:al
3		wv 64	. . . . . . . 8 |- y:al:al
4	2, 3	weqi 76	. . . . . . 7 |- [x:al = y:al]:*
5		weq 41	. . . . . . . 8 |- = :(al -> (al -> *))
6	5, 2, 1	wov 72	. . . . . . . . 9 |- [x:al = z:al]:*
7	6	id 25	. . . . . . . 8 |- [x:al = z:al] |= [x:al = z:al]
8	5, 2, 3, 7	oveq1 99	. . . . . . 7 |- [x:al = z:al] |= [[x:al = y:al] = [z:al = y:al]]
9	4, 1, 8	cla4v 152	. . . . . 6 |- (A.\x:al [x:al = y:al]) |= [z:al = y:al]
10	4	ax4 150	. . . . . . 7 |- (A.\x:al [x:al = y:al]) |= [x:al = y:al]
11	2, 10	eqcomi 79	. . . . . 6 |- (A.\x:al [x:al = y:al]) |= [y:al = x:al]
12	1, 9, 11	eqtri 95	. . . . 5 |- (A.\x:al [x:al = y:al]) |= [z:al = x:al]
13	12	alrimiv 151	. . . 4 |- (A.\x:al [x:al = y:al]) |= (A.\z:al [z:al = x:al])
14		wal 134	. . . . . 6 |- A.:((al -> *) -> *)
15	4	wl 66	. . . . . 6 |- \x:al [x:al = y:al]:(al -> *)
16	14, 15	wc 50	. . . . 5 |- (A.\x:al [x:al = y:al]):*
17	3, 2	weqi 76	. . . . . . 7 |- [y:al = x:al]:*
18	17	wl 66	. . . . . 6 |- \y:al [y:al = x:al]:(al -> *)
19	3, 1	weqi 76	. . . . . . . . 9 |- [y:al = z:al]:*
20	19	id 25	. . . . . . . 8 |- [y:al = z:al] |= [y:al = z:al]
21	5, 3, 2, 20	oveq1 99	. . . . . . 7 |- [y:al = z:al] |= [[y:al = x:al] = [z:al = x:al]]
22	17, 21	cbv 180	. . . . . 6 |- T. |= [\y:al [y:al = x:al] = \z:al [z:al = x:al]]
23	14, 18, 22	ceq2 90	. . . . 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 87	. . 3 |- (A.\x:al [x:al = y:al]) |= (A.\y:al [y:al = x:al])
26		wtru 43	. . 3 |- T.:*
27	25, 26	adantl 56	. 2 |- (T., (A.\x:al [x:al = y:al])) |= (A.\y:al [y:al = x:al])
28	27	ex 158	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 121  A.tal 122

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-wctl 31  ax-wctr 32  ax-weq 40  ax-refl 42  ax-eqmp 45  ax-ded 46  ax-wct 47  ax-wc 49  ax-ceq 51  ax-wv 63  ax-wl 65  ax-beta 67  ax-distrc 68  ax-leq 69  ax-distrl 70  ax-wov 71  ax-eqtypi 77  ax-eqtypri 80  ax-hbl1 103  ax-17 105  ax-inst 113  ax-eta 177

This theorem depends on definitions:  df-ov 73  df-al 126  df-an 128  df-im 129

This theorem is referenced by: (None)