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

Theorem ralcom 3078
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 2750 . 2 𝑦𝐴
2 nfcv 2750 . 2 𝑥𝐵
31, 2ralcomf 3076 1 (∀𝑥𝐴𝑦𝐵 𝜑 ↔ ∀𝑦𝐵𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 194  wral 2895
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ral 2900
This theorem is referenced by:  ralcom4  3196  ssint  4422  iinrab2  4513  disjxun  4575  reusv3  4797  cnvpo  5576  cnvso  5577  fununi  5864  isocnv2  6459  dfsmo2  7308  ixpiin  7797  boxriin  7813  dedekind  10051  rexfiuz  13881  gcdcllem1  15005  mreacs  16088  comfeq  16135  catpropd  16138  isnsg2  17393  cntzrec  17535  oppgsubm  17561  opprirred  18471  opprsubrg  18570  islindf4  19938  cpmatmcllem  20284  tgss2  20544  ist1-2  20903  kgencn  21111  ptcnplem  21176  cnmptcom  21233  fbun  21396  cnflf  21558  fclsopn  21570  cnfcf  21598  isclmp  22636  isncvsngp  22683  caucfil  22807  ovolgelb  22972  dyadmax  23089  ftc1a  23521  ulmcau  23870  perpcom  25326  colinearalg  25508  frgrawopreg2  26344  phoeqi  26903  ho02i  27878  hoeq2  27880  adjsym  27882  cnvadj  27941  mddmd2  28358  cdj3lem3b  28489  cvmlift2lem12  30356  dfpo2  30704  elpotr  30736  poimirlem29  32411  heicant  32417  ispsubsp2  33853  ntrclsiso  37188  ntrneiiso  37212  ntrneik2  37213  ntrneix2  37214  ntrneik3  37217  ntrneix3  37218  ntrneik13  37219  ntrneix13  37220  ntrneik4w  37221  hbra2VD  37921  2reu4a  39642  uhgrvd00  40752  pthdlem2lem  40975  frgrwopreg2  41490
  Copyright terms: Public domain W3C validator