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

Theorem ralcom 3079
Description: Commutation of restricted universal quantifiers. (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 nfcv 2751 . 2 𝑦𝐴
2 nfcv 2751 . 2 𝑥𝐵
31, 2ralcomf 3077 1 (∀𝑥𝐴𝑦𝐵 𝜑 ↔ ∀𝑦𝐵𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 195  wral 2896
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901
This theorem is referenced by:  ralcom4  3197  ssint  4428  iinrab2  4519  disjxun  4581  reusv3  4802  cnvpo  5590  cnvso  5591  fununi  5878  isocnv2  6481  dfsmo2  7331  ixpiin  7820  boxriin  7836  dedekind  10079  rexfiuz  13935  gcdcllem1  15059  mreacs  16142  comfeq  16189  catpropd  16192  isnsg2  17447  cntzrec  17589  oppgsubm  17615  opprirred  18525  opprsubrg  18624  islindf4  19996  cpmatmcllem  20342  tgss2  20602  ist1-2  20961  kgencn  21169  ptcnplem  21234  cnmptcom  21291  fbun  21454  cnflf  21616  fclsopn  21628  cnfcf  21656  isclmp  22705  isncvsngp  22757  caucfil  22889  ovolgelb  23055  dyadmax  23172  ftc1a  23604  ulmcau  23953  perpcom  25408  colinearalg  25590  frgrawopreg2  26578  phoeqi  27097  ho02i  28072  hoeq2  28074  adjsym  28076  cnvadj  28135  mddmd2  28552  cdj3lem3b  28683  cvmlift2lem12  30550  dfpo2  30898  elpotr  30930  poimirlem29  32608  heicant  32614  ispsubsp2  34050  ntrclsiso  37385  ntrneiiso  37409  ntrneik2  37410  ntrneix2  37411  ntrneik3  37414  ntrneix3  37415  ntrneik13  37416  ntrneix13  37417  ntrneik4w  37418  hbra2VD  38118  2reu4a  39838  uhgrvd00  40750  pthdlem2lem  40973  frgrwopreg2  41488
  Copyright terms: Public domain W3C validator