MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ralcom Structured version   Visualization version   GIF version

Theorem ralcom 3339
Description: Commutation of restricted universal quantifiers. See ralcom2 3348 for a version without disjoint variable condition on 𝑥, 𝑦. This theorem should be used in place of ralcom2 3348 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
StepHypRef Expression
1 ancomst 468 . . . 4 (((𝑥𝐴𝑦𝐵) → 𝜑) ↔ ((𝑦𝐵𝑥𝐴) → 𝜑))
212albii 1822 . . 3 (∀𝑥𝑦((𝑥𝐴𝑦𝐵) → 𝜑) ↔ ∀𝑥𝑦((𝑦𝐵𝑥𝐴) → 𝜑))
3 alcom 2164 . . 3 (∀𝑥𝑦((𝑦𝐵𝑥𝐴) → 𝜑) ↔ ∀𝑦𝑥((𝑦𝐵𝑥𝐴) → 𝜑))
42, 3bitri 278 . 2 (∀𝑥𝑦((𝑥𝐴𝑦𝐵) → 𝜑) ↔ ∀𝑦𝑥((𝑦𝐵𝑥𝐴) → 𝜑))
5 r2al 3189 . 2 (∀𝑥𝐴𝑦𝐵 𝜑 ↔ ∀𝑥𝑦((𝑥𝐴𝑦𝐵) → 𝜑))
6 r2al 3189 . 2 (∀𝑦𝐵𝑥𝐴 𝜑 ↔ ∀𝑦𝑥((𝑦𝐵𝑥𝐴) → 𝜑))
74, 5, 63bitr4i 306 1 (∀𝑥𝐴𝑦𝐵 𝜑 ↔ ∀𝑦𝐵𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  wal 1536  wcel 2115  wral 3126
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-11 2162
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-ral 3131
This theorem is referenced by:  ralcom13  3344  ralrot3  3346  ralcom4OLD  3502  2reu4lem  4438  ssint  4865  iinrab2  4965  disjxun  5037  reusv3  5279  cnvpo  6111  cnvso  6112  fununi  6402  isocnv2  7058  dfsmo2  7959  tz7.48lem  8052  ixpiin  8463  boxriin  8479  dedekind  10780  rexfiuz  14686  gcdcllem1  15825  mreacs  16907  comfeq  16954  catpropd  16957  isnsg2  18286  cntzrec  18442  oppgsubm  18468  opprirred  19430  opprsubrg  19531  rmodislmodlem  19676  rmodislmod  19677  islindf4  20957  cpmatmcllem  21301  tgss2  21570  ist1-2  21930  kgencn  22139  ptcnplem  22204  cnmptcom  22261  fbun  22423  cnflf  22585  fclsopn  22597  cnfcf  22625  isclmp  23680  isncvsngp  23732  caucfil  23865  ovolgelb  24062  dyadmax  24180  ftc1a  24618  ulmcau  24968  perpcom  26485  colinearalg  26682  uhgrvd00  27302  pthdlem2lem  27534  frgrwopregbsn  28080  phoeqi  28618  ho02i  29590  hoeq2  29592  adjsym  29594  cnvadj  29653  mddmd2  30070  cdj3lem3b  30201  mcgcnv  30665  cvmlift2lem12  32568  dfpo2  32998  elpotr  33033  noetalem3  33226  conway  33271  fvineqsnf1  34707  poimirlem29  34964  heicant  34970  ispsubsp2  36920  ntrclsiso  40552  ntrneiiso  40576  ntrneik2  40577  ntrneix2  40578  ntrneik3  40581  ntrneix3  40582  ntrneik13  40583  ntrneix13  40584  ntrneik4w  40585  imo72b2  40660  tratrb  41025  hbra2VD  41349  tratrbVD  41350
  Copyright terms: Public domain W3C validator