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	⊢ (∀x ∈ A ∀y ∈ A φ → ∀y ∈ A ∀x ∈ A φ)

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

Proof of Theorem ralcom2

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

Syntax hints:  ¬ wn 1   → wi 2   ↔ wb 127  ∀wal 672   = weq 797   ∈ wcel 1092  ∀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