Theorem ralcom 1821

Description: Commutation of restricted quantifiers.

Assertion

Ref	Expression
ralcom	⊢ (∀x ∈ A ∀y ∈ B φ ↔ ∀y ∈ B ∀x ∈ A φ)

Distinct variable groups:   x,y   x,B   y,A

Proof of Theorem ralcom

Step	Hyp	Ref	Expression
1		ancom 446	. . . . 5 ⊢ ((x ∈ A ⋀ y ∈ B) ↔ (y ∈ B ⋀ x ∈ A))
2	1	imbi1i 193	. . . 4 ⊢ (((x ∈ A ⋀ y ∈ B) → φ) ↔ ((y ∈ B ⋀ x ∈ A) → φ))
3	2	2albii 1041	. . 3 ⊢ (∀x∀y((x ∈ A ⋀ y ∈ B) → φ) ↔ ∀x∀y((y ∈ B ⋀ x ∈ A) → φ))
4		alcom 1073	. . 3 ⊢ (∀x∀y((y ∈ B ⋀ x ∈ A) → φ) ↔ ∀y∀x((y ∈ B ⋀ x ∈ A) → φ))
5	3, 4	bitri 180	. 2 ⊢ (∀x∀y((x ∈ A ⋀ y ∈ B) → φ) ↔ ∀y∀x((y ∈ B ⋀ x ∈ A) → φ))
6		r2al 1723	. 2 ⊢ (∀x ∈ A ∀y ∈ B φ ↔ ∀x∀y((x ∈ A ⋀ y ∈ B) → φ))
7		r2al 1723	. 2 ⊢ (∀y ∈ B ∀x ∈ A φ ↔ ∀y∀x((y ∈ B ⋀ x ∈ A) → φ))
8	5, 6, 7	3bitr4i 190	1 ⊢ (∀x ∈ A ∀y ∈ B φ ↔ ∀y ∈ B ∀x ∈ A φ)

Syntax hints:   → wi 3   ↔ wb 153   ⋀ wa 230  ∀wal 995   ∈ wcel 999  ∀wral 1692

This theorem is referenced by:  ralcom4 1870  ssint 2603  cnvpo 3579  cnvso 3580  fununi 3620  mapxpen 4560  cau3ii 7004  fsumcom 7118  tgss3 7727  basgen2 7728  cncnp 7863  phoeqi 8602  occli 9264  ho02i 9838  hoeq2 9840  adjsym 9842  cnvadj 9899  hhlnoi 9909  mddmd2 10320  cdj3lem3b 10451

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019

This theorem depends on definitions:  df-bi 154  df-an 232  df-ral 1696

Copyright terms: Public domain