Theorem ralcom 3290

Description: Commutation of restricted universal quantifiers. See ralcom2 3362 for a version without disjoint variable condition on 𝑥, 𝑦. This theorem should be used in place of ralcom2 3362 since it depends on a smaller set of axioms. (Contributed by NM, 13-Oct-1999.) (Revised by Mario Carneiro, 14-Oct-2016.)

Assertion

Ref	Expression
ralcom	⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 𝜑)

Distinct variable groups:   𝑥,𝑦   𝑦,𝐴   𝑥,𝐵

Allowed substitution hints:   𝜑(𝑥, 𝑦)   𝐴(𝑥)   𝐵(𝑦)

Proof of Theorem ralcom

Step	Hyp	Ref	Expression
1		ancomst 470	. . . 4 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑) ↔ ((𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝜑))
2	1	2albii 1853	. . 3 ⊢ (∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑) ↔ ∀𝑥∀𝑦((𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝜑))
3		alcom 2196	. . 3 ⊢ (∀𝑥∀𝑦((𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝜑) ↔ ∀𝑦∀𝑥((𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝜑))
4	2, 3	bitri 278	. 2 ⊢ (∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑) ↔ ∀𝑦∀𝑥((𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝜑))
5		r2al 3198	. 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑))
6		r2al 3198	. 2 ⊢ (∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦∀𝑥((𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → 𝜑))
7	4, 5, 6	3bitr4i 306	1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 𝜑)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1568   ∈ wcel 2145  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-11 2194

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-ral 3077

This theorem is used by:  rexcom  3291  ralrot3  3293  ralcom13  3294  2reu4lem  4479  ssint  4924  iinrab2  5028  disjxun  5101  reusv3  5370  cnvpo  6285  cnvso  6286  dfpo2  6294  fununi  6609  isocnv2  7333  dfsmo2  8337  tz7.48lem  8431  ixpiin  8932  boxriin  8948  dedekind  11398  rexfiuz  15436  gcdcllem1  16590  mreacs  17747  comfeq  17795  catpropd  17798  isnsg2  19280  cntzrec  19464  oppgsubm  19490  opprirred  20564  opprsubrng  20722  opprsubrg  20756  opprdomnb  20879  rmodislmodlem  21114  rmodislmod  21115  islindf4  22052  cpmatmcllem  22944  tgss2  23213  ist1-2  23573  kgencn  23783  ptcnplem  23848  cnmptcom  23905  fbun  24067  cnflf  24229  fclsopn  24241  cnfcf  24269  isclmp  25326  isncvsngp  25378  caucfil  25512  ovolgelb  25709  dyadmax  25827  ftc1a  26265  ulmcau  26632  noetasuplem4  27973  conway  28045  cofcutr  28190  addsprop  28242  onsfi  28622  perpcom  29068  colinearalg  29368  uhgrvd00  29995  pthdlem2lem  30233  frgrwopregbsn  30798  phoeqi  31339  ho02i  32311  hoeq2  32313  adjsym  32315  cnvadj  32374  mddmd2  32791  cdj3lem3b  32922  mgccnv  33440  cvmlift2lem12  35894  elpotr  36359  nmulcom  36775  fvineqsnf1  38165  poimirlem29  38399  heicant  38405  disjimeceqim  39553  ispsubsp2  40620  fsuppind  43437  nla0003  44266  ntrclsiso  44908  ntrneiiso  44932  ntrneik2  44933  ntrneix2  44934  ntrneik3  44937  ntrneix3  44938  ntrneik13  44939  ntrneix13  44940  ntrneik4w  44941  imo72b2  45013  tratrb  45360  hbra2VD  45683  tratrbVD  45684  termopropd  50171