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

Theorem ralcom 3280
Description: Commutation of restricted universal quantifiers. See ralcom2 3288 for a version without disjoint variable condition on 𝑥, 𝑦. This theorem should be used in place of ralcom2 3288 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 1828 . . 3 (∀𝑥𝑦((𝑥𝐴𝑦𝐵) → 𝜑) ↔ ∀𝑥𝑦((𝑦𝐵𝑥𝐴) → 𝜑))
3 alcom 2161 . . 3 (∀𝑥𝑦((𝑦𝐵𝑥𝐴) → 𝜑) ↔ ∀𝑦𝑥((𝑦𝐵𝑥𝐴) → 𝜑))
42, 3bitri 278 . 2 (∀𝑥𝑦((𝑥𝐴𝑦𝐵) → 𝜑) ↔ ∀𝑦𝑥((𝑦𝐵𝑥𝐴) → 𝜑))
5 r2al 3123 . 2 (∀𝑥𝐴𝑦𝐵 𝜑 ↔ ∀𝑥𝑦((𝑥𝐴𝑦𝐵) → 𝜑))
6 r2al 3123 . 2 (∀𝑦𝐵𝑥𝐴 𝜑 ↔ ∀𝑦𝑥((𝑦𝐵𝑥𝐴) → 𝜑))
74, 5, 63bitr4i 306 1 (∀𝑥𝐴𝑦𝐵 𝜑 ↔ ∀𝑦𝐵𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  wal 1541  wcel 2111  wral 3062
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-11 2159
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-ral 3067
This theorem is referenced by:  ralcom13  3284  ralrot3  3286  2reu4lem  4452  ssint  4890  iinrab2  4993  disjxun  5066  reusv3  5313  cnvpo  6165  cnvso  6166  dfpo2  6174  fununi  6473  isocnv2  7159  dfsmo2  8105  tz7.48lem  8198  ixpiin  8626  boxriin  8642  dedekind  11020  rexfiuz  14936  gcdcllem1  16083  mreacs  17186  comfeq  17234  catpropd  17237  isnsg2  18597  cntzrec  18753  oppgsubm  18779  opprirred  19745  opprsubrg  19846  rmodislmodlem  19991  rmodislmod  19992  islindf4  20825  cpmatmcllem  21639  tgss2  21908  ist1-2  22268  kgencn  22477  ptcnplem  22542  cnmptcom  22599  fbun  22761  cnflf  22923  fclsopn  22935  cnfcf  22963  isclmp  24018  isncvsngp  24070  caucfil  24204  ovolgelb  24401  dyadmax  24519  ftc1a  24958  ulmcau  25311  perpcom  26828  colinearalg  27025  uhgrvd00  27646  pthdlem2lem  27878  frgrwopregbsn  28424  phoeqi  28962  ho02i  29934  hoeq2  29936  adjsym  29938  cnvadj  29997  mddmd2  30414  cdj3lem3b  30545  mgccnv  31020  cvmlift2lem12  33012  elpotr  33499  noetasuplem4  33702  conway  33756  cofcutr  33855  fvineqsnf1  35345  poimirlem29  35570  heicant  35576  ispsubsp2  37524  fsuppind  40018  ntrclsiso  41383  ntrneiiso  41407  ntrneik2  41408  ntrneix2  41409  ntrneik3  41412  ntrneix3  41413  ntrneik13  41414  ntrneix13  41415  ntrneik4w  41416  imo72b2  41490  tratrb  41858  hbra2VD  42182  tratrbVD  42183
  Copyright terms: Public domain W3C validator