Theorem ralcom 3291

Description: Commutation of restricted universal quantifiers. See ralcom2 3363 for a version without disjoint variable condition on 𝑥, 𝑦. This theorem should be used in place of ralcom2 3363 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 3199	. 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑))
6		r2al 3199	. 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 3077

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 3078

This theorem is used by:  rexcom  3292  ralrot3  3294  ralcom13  3295  2reu4lem  4479  ssint  4924  iinrab2  5028  disjxun  5101  reusv3  5367  cnvpo  6291  cnvso  6292  dfpo2  6300  fununi  6616  isocnv2  7340  dfsmo2  8356  tz7.48lemOLD  8452  ixpiin  8953  boxriin  8969  dedekind  11474  rexfiuz  15516  gcdcllem1  16670  mreacs  17833  comfeq  17881  catpropd  17884  isnsg2  19367  cntzrec  19551  oppgsubm  19577  opprirred  20653  opprsubrng  20812  opprsubrg  20846  opprdomnb  20969  rmodislmodlem  21205  rmodislmod  21206  islindf4  22145  cpmatmcllem  23037  tgss2  23306  ist1-2  23666  kgencn  23876  ptcnplem  23941  cnmptcom  23998  fbun  24160  cnflf  24322  fclsopn  24334  cnfcf  24362  isclmp  25419  isncvsngp  25471  caucfil  25605  ovolgelb  25802  dyadmax  25920  ftc1a  26358  ulmcau  26723  noetasuplem4  28094  conway  28166  cofcutr  28311  addsprop  28363  onsfi  28743  perpcom  29189  colinearalg  29489  uhgrvd00  30116  pthdlem2lem  30354  frgrwopregbsn  30919  phoeqi  31460  ho02i  32432  hoeq2  32434  adjsym  32436  cnvadj  32495  mddmd2  32912  cdj3lem3b  33043  mgccnv  33561  cvmlift2lem12  36080  elpotr  36544  nmulcom  36944  fvineqsnf1  38335  poimirlem29  38569  heicant  38575  disjimeceqim  39738  ispsubsp2  40805  fsuppind  43620  nla0003  44427  ntrclsiso  45068  ntrneiiso  45092  ntrneik2  45093  ntrneix2  45094  ntrneik3  45097  ntrneix3  45098  ntrneik13  45099  ntrneix13  45100  ntrneik4w  45101  imo72b2  45173  tratrb  45520  hbra2VD  45843  tratrbVD  45844  termopropd  50353