Theorem ralcom2 1314

Description: Commutation of restricted quantifiers. Note that x and y needn't be distinct (this makes the proof longer but illustrates the use of ddelim 1000).

Assertion

Ref	Expression
ralcom2	|- (A.x e. A A.y e. A ph -> A.y e. A A.x e. A ph)

Distinct variable group(s):   y,A   x,A

Proof of Theorem ralcom2

Step	Hyp	Ref	Expression
1		id 9	. . . 4 |- (A.x(x e. A -> A.x(x e. A -> ph)) -> A.x(x e. A -> A.x(x e. A -> ph)))
2		eq5 824	. . . . . 6 |- (A.x x = y -> A.xA.x x = y)
3		eleq1 1149	. . . . . . . . . 10 |- (x = y -> (x e. A <-> y e. A))
4	3	a4s 682	. . . . . . . . 9 |- (A.x x = y -> (x e. A <-> y e. A))
5	4	imbi1d 465	. . . . . . . 8 |- (A.x x = y -> ((x e. A -> ph) <-> (y e. A -> ph)))
6	5	del34b 837	. . . . . . 7 |- (A.x x = y -> (A.x(x e. A -> ph) <-> A.y(y e. A -> ph)))
7	6	imbi2d 464	. . . . . 6 |- (A.x x = y -> ((x e. A -> A.x(x e. A -> ph)) <-> (x e. A -> A.y(y e. A -> ph))))
8	2, 7	biald 782	. . . . 5 |- (A.x x = y -> (A.x(x e. A -> A.x(x e. A -> ph)) <-> A.x(x e. A -> A.y(y e. A -> ph))))
9	4	imbi1d 465	. . . . . 6 |- (A.x x = y -> ((x e. A -> A.x(x e. A -> ph)) <-> (y e. A -> A.x(x e. A -> ph))))
10	9	del34b 837	. . . . 5 |- (A.x x = y -> (A.x(x e. A -> A.x(x e. A -> ph)) <-> A.y(y e. A -> A.x(x e. A -> ph))))
11	8, 10	imbi12d 474	. . . 4 |- (A.x x = y -> ((A.x(x e. A -> A.x(x e. A -> ph)) -> A.x(x e. A -> A.x(x e. A -> ph))) <-> (A.x(x e. A -> A.y(y e. A -> ph)) -> A.y(y e. A -> A.x(x e. A -> ph)))))
12	1, 11	mpbii 168	. . 3 |- (A.x x = y -> (A.x(x e. A -> A.y(y e. A -> ph)) -> A.y(y e. A -> A.x(x e. A -> ph))))
13		eq6 826	. . . . . . 7 |- (-. A.x x = y -> A.x -. A.x x = y)
14	13	hbal 700	. . . . . 6 |- (A.y -. A.x x = y -> A.xA.y -. A.x x = y)
15		eq6 826	. . . . . . . 8 |- (-. A.x x = y -> A.y -. A.x x = y)
16		ax-17 925	. . . . . . . . . 10 |- (z e. A -> A.y z e. A)
17		eleq1 1149	. . . . . . . . . 10 |- (z = x -> (z e. A <-> x e. A))
18	16, 17	ddelim 1000	. . . . . . . . 9 |- (-. A.y y = x -> (x e. A -> A.y x e. A))
19	18	eq4ds 823	. . . . . . . 8 |- (-. A.x x = y -> (x e. A -> A.y x e. A))
20		hba1 698	. . . . . . . . 9 |- (A.y(y e. A -> ph) -> A.yA.y(y e. A -> ph))
21	20	a1i 7	. . . . . . . 8 |- (-. A.x x = y -> (A.y(y e. A -> ph) -> A.yA.y(y e. A -> ph)))
22	15, 19, 21	hbimd 787	. . . . . . 7 |- (-. A.x x = y -> ((x e. A -> A.y(y e. A -> ph)) -> A.y(x e. A -> A.y(y e. A -> ph))))
23	22	a4s 682	. . . . . 6 |- (A.y -. A.x x = y -> ((x e. A -> A.y(y e. A -> ph)) -> A.y(x e. A -> A.y(y e. A -> ph))))
24	14, 23	hbald 790	. . . . 5 |- (A.y -. A.x x = y -> (A.x(x e. A -> A.y(y e. A -> ph)) -> A.yA.x(x e. A -> A.y(y e. A -> ph))))
25		ax-17 925	. . . . . . . 8 |- (z e. A -> A.x z e. A)
26		eleq1 1149	. . . . . . . 8 |- (z = y -> (z e. A <-> y e. A))
27	25, 26	ddelim 1000	. . . . . . 7 |- (-. A.x x = y -> (y e. A -> A.x y e. A))
28		ax-4 673	. . . . . . . . . 10 |- (A.y(y e. A -> ph) -> (y e. A -> ph))
29	28	syl3 18	. . . . . . . . 9 |- ((x e. A -> A.y(y e. A -> ph)) -> (x e. A -> (y e. A -> ph)))
30	29	com23 32	. . . . . . . 8 |- ((x e. A -> A.y(y e. A -> ph)) -> (y e. A -> (x e. A -> ph)))
31	30	19.20ii 692	. . . . . . 7 |- (A.x(x e. A -> A.y(y e. A -> ph)) -> (A.x y e. A -> A.x(x e. A -> ph)))
32	27, 31	syl9 55	. . . . . 6 |- (-. A.x x = y -> (A.x(x e. A -> A.y(y e. A -> ph)) -> (y e. A -> A.x(x e. A -> ph))))
33	32	19.20ii 692	. . . . 5 |- (A.y -. A.x x = y -> (A.yA.x(x e. A -> A.y(y e. A -> ph)) -> A.y(y e. A -> A.x(x e. A -> ph))))
34	24, 33	syld 27	. . . 4 |- (A.y -. A.x x = y -> (A.x(x e. A -> A.y(y e. A -> ph)) -> A.y(y e. A -> A.x(x e. A -> ph))))
35	34	eq6s 827	. . 3 |- (-. A.x x = y -> (A.x(x e. A -> A.y(y e. A -> ph)) -> A.y(y e. A -> A.x(x e. A -> ph))))
36	12, 35	pm2.61i 110	. 2 |- (A.x(x e. A -> A.y(y e. A -> ph)) -> A.y(y e. A -> A.x(x e. A -> ph)))
37		df-ral 1205	. . 3 |- (A.x e. A A.y e. A ph <-> A.x(x e. A -> A.y e. A ph))
38		df-ral 1205	. . . . 5 |- (A.y e. A ph <-> A.y(y e. A -> ph))
39	38	imbi2i 160	. . . 4 |- ((x e. A -> A.y e. A ph) <-> (x e. A -> A.y(y e. A -> ph)))
40	39	bial 695	. . 3 |- (A.x(x e. A -> A.y e. A ph) <-> A.x(x e. A -> A.y(y e. A -> ph)))
41	37, 40	bitr 151	. 2 |- (A.x e. A A.y e. A ph <-> A.x(x e. A -> A.y(y e. A -> ph)))
42		df-ral 1205	. . 3 |- (A.y e. A A.x e. A ph <-> A.y(y e. A -> A.x e. A ph))
43		df-ral 1205	. . . . 5 |- (A.x e. A ph <-> A.x(x e. A -> ph))
44	43	imbi2i 160	. . . 4 |- ((y e. A -> A.x e. A ph) <-> (y e. A -> A.x(x e. A -> ph)))
45	44	bial 695	. . 3 |- (A.y(y e. A -> A.x e. A ph) <-> A.y(y e. A -> A.x(x e. A -> ph)))
46	42, 45	bitr 151	. 2 |- (A.y e. A A.x e. A ph <-> A.y(y e. A -> A.x(x e. A -> ph)))
47	36, 41, 46	3imtr4 192	1 |- (A.x e. A A.y e. A ph -> A.y e. A A.x e. A ph)

Syntax hints:  -. wn 1   -> wi 2   <-> wb 127  A.wal 672   = weq 797   e. wcel 1092  A.wral 1201

This theorem is referenced by:  tz7.48lem 2993

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853  df-cleq 1097  df-clel 1099  df-ral 1205

metamath.org