Theorem ralcom2 2776

Description: Commutation of restricted quantifiers. Note that x and y needn't be distinct (this makes the proof longer). (Contributed by NM, 24-Nov-1994.) (Proof shortened by Mario Carneiro, 17-Oct-2016.)

Assertion

Ref	Expression
ralcom2	⊢ (∀x ∈ A ∀y ∈ A φ → ∀y ∈ A ∀x ∈ A φ)

Distinct variable groups:   y,A   x,A

Allowed substitution hints:   φ(x, y)

Proof of Theorem ralcom2

Step	Hyp	Ref	Expression
1		eleq1 2413	. . . . . . 7 ⊢ (x = y → (x ∈ A ↔ y ∈ A))
2	1	sps 1754	. . . . . 6 ⊢ (∀x x = y → (x ∈ A ↔ y ∈ A))
3	2	imbi1d 308	. . . . . . . . 9 ⊢ (∀x x = y → ((x ∈ A → φ) ↔ (y ∈ A → φ)))
4	3	dral1 1965	. . . . . . . 8 ⊢ (∀x x = y → (∀x(x ∈ A → φ) ↔ ∀y(y ∈ A → φ)))
5	4	bicomd 192	. . . . . . 7 ⊢ (∀x x = y → (∀y(y ∈ A → φ) ↔ ∀x(x ∈ A → φ)))
6		df-ral 2620	. . . . . . 7 ⊢ (∀y ∈ A φ ↔ ∀y(y ∈ A → φ))
7		df-ral 2620	. . . . . . 7 ⊢ (∀x ∈ A φ ↔ ∀x(x ∈ A → φ))
8	5, 6, 7	3bitr4g 279	. . . . . 6 ⊢ (∀x x = y → (∀y ∈ A φ ↔ ∀x ∈ A φ))
9	2, 8	imbi12d 311	. . . . 5 ⊢ (∀x x = y → ((x ∈ A → ∀y ∈ A φ) ↔ (y ∈ A → ∀x ∈ A φ)))
10	9	dral1 1965	. . . 4 ⊢ (∀x x = y → (∀x(x ∈ A → ∀y ∈ A φ) ↔ ∀y(y ∈ A → ∀x ∈ A φ)))
11		df-ral 2620	. . . 4 ⊢ (∀x ∈ A ∀y ∈ A φ ↔ ∀x(x ∈ A → ∀y ∈ A φ))
12		df-ral 2620	. . . 4 ⊢ (∀y ∈ A ∀x ∈ A φ ↔ ∀y(y ∈ A → ∀x ∈ A φ))
13	10, 11, 12	3bitr4g 279	. . 3 ⊢ (∀x x = y → (∀x ∈ A ∀y ∈ A φ ↔ ∀y ∈ A ∀x ∈ A φ))
14	13	biimpd 198	. 2 ⊢ (∀x x = y → (∀x ∈ A ∀y ∈ A φ → ∀y ∈ A ∀x ∈ A φ))
15		nfnae 1956	. . . . 5 ⊢ Ⅎy ¬ ∀x x = y
16		nfra2 2669	. . . . 5 ⊢ Ⅎy∀x ∈ A ∀y ∈ A φ
17	15, 16	nfan 1824	. . . 4 ⊢ Ⅎy(¬ ∀x x = y ∧ ∀x ∈ A ∀y ∈ A φ)
18		nfnae 1956	. . . . . . . 8 ⊢ Ⅎx ¬ ∀x x = y
19		nfra1 2665	. . . . . . . 8 ⊢ Ⅎx∀x ∈ A ∀y ∈ A φ
20	18, 19	nfan 1824	. . . . . . 7 ⊢ Ⅎx(¬ ∀x x = y ∧ ∀x ∈ A ∀y ∈ A φ)
21		nfcvf 2512	. . . . . . . . 9 ⊢ (¬ ∀x x = y → Ⅎxy)
22	21	adantr 451	. . . . . . . 8 ⊢ ((¬ ∀x x = y ∧ ∀x ∈ A ∀y ∈ A φ) → Ⅎxy)
23		nfcvd 2491	. . . . . . . 8 ⊢ ((¬ ∀x x = y ∧ ∀x ∈ A ∀y ∈ A φ) → ℲxA)
24	22, 23	nfeld 2505	. . . . . . 7 ⊢ ((¬ ∀x x = y ∧ ∀x ∈ A ∀y ∈ A φ) → Ⅎx y ∈ A)
25	20, 24	nfan1 1881	. . . . . 6 ⊢ Ⅎx((¬ ∀x x = y ∧ ∀x ∈ A ∀y ∈ A φ) ∧ y ∈ A)
26		rsp2 2677	. . . . . . . . 9 ⊢ (∀x ∈ A ∀y ∈ A φ → ((x ∈ A ∧ y ∈ A) → φ))
27	26	ancomsd 440	. . . . . . . 8 ⊢ (∀x ∈ A ∀y ∈ A φ → ((y ∈ A ∧ x ∈ A) → φ))
28	27	expdimp 426	. . . . . . 7 ⊢ ((∀x ∈ A ∀y ∈ A φ ∧ y ∈ A) → (x ∈ A → φ))
29	28	adantll 694	. . . . . 6 ⊢ (((¬ ∀x x = y ∧ ∀x ∈ A ∀y ∈ A φ) ∧ y ∈ A) → (x ∈ A → φ))
30	25, 29	ralrimi 2696	. . . . 5 ⊢ (((¬ ∀x x = y ∧ ∀x ∈ A ∀y ∈ A φ) ∧ y ∈ A) → ∀x ∈ A φ)
31	30	ex 423	. . . 4 ⊢ ((¬ ∀x x = y ∧ ∀x ∈ A ∀y ∈ A φ) → (y ∈ A → ∀x ∈ A φ))
32	17, 31	ralrimi 2696	. . 3 ⊢ ((¬ ∀x x = y ∧ ∀x ∈ A ∀y ∈ A φ) → ∀y ∈ A ∀x ∈ A φ)
33	32	ex 423	. 2 ⊢ (¬ ∀x x = y → (∀x ∈ A ∀y ∈ A φ → ∀y ∈ A ∀x ∈ A φ))
34	14, 33	pm2.61i 156	1 ⊢ (∀x ∈ A ∀y ∈ A φ → ∀y ∈ A ∀x ∈ A φ)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 176   ∧ wa 358  ∀wal 1540   = wceq 1642   ∈ wcel 1710  Ⅎwnfc 2477  ∀wral 2615

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334

This proof depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-cleq 2346  df-clel 2349  df-nfc 2479  df-ral 2620

This theorem is used by: (None)