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

Theorem ralcom 2983
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 2655 . 2 𝑦𝐴
2 nfcv 2655 . 2 𝑥𝐵
31, 2ralcomf 2981 1 (∀𝑥𝐴𝑦𝐵 𝜑 ↔ ∀𝑦𝐵𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 194  wral 2800
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-ex 1695  df-nf 1699  df-sb 1831  df-cleq 2507  df-clel 2510  df-nfc 2644  df-ral 2805
This theorem is referenced by:  ralcom4  3101  ssint  4326  iinrab2  4417  disjxun  4479  reusv3  4701  cnvpo  5480  cnvso  5481  fununi  5763  isocnv2  6357  dfsmo2  7206  ixpiin  7695  boxriin  7711  dedekind  9950  rexfiuz  13792  gcdcllem1  14930  mreacs  16032  comfeq  16079  catpropd  16082  isnsg2  17337  cntzrec  17479  oppgsubm  17505  opprirred  18430  opprsubrg  18529  islindf4  19897  cpmatmcllem  20243  tgss2  20503  ist1-2  20862  kgencn  21070  ptcnplem  21135  cnmptcom  21192  fbun  21355  cnflf  21517  fclsopn  21529  cnfcf  21557  caucfil  22754  ovolgelb  22931  dyadmax  23048  ftc1a  23480  ulmcau  23841  perpcom  25299  colinearalg  25481  frgrawopreg2  26317  phoeqi  26876  ho02i  27861  hoeq2  27863  adjsym  27865  cnvadj  27924  mddmd2  28341  cdj3lem3b  28472  cvmlift2lem12  30396  dfpo2  30741  elpotr  30773  poimirlem29  32483  heicant  32489  ispsubsp2  33925  ntrclsiso  37267  ntrneiiso  37291  ntrneik2  37292  ntrneix2  37293  ntrneik3  37296  ntrneix3  37297  ntrneik13  37298  ntrneix13  37299  ntrneik4w  37300  hbra2VD  38000  2reu4a  39732  uhgrvd00  40842  pthdlem2lem  41065  frgrwopreg2  41580
  Copyright terms: Public domain W3C validator