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

Theorem ralcom 3092
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 2761 . 2 𝑦𝐴
2 nfcv 2761 . 2 𝑥𝐵
31, 2ralcomf 3090 1 (∀𝑥𝐴𝑦𝐵 𝜑 ↔ ∀𝑦𝐵𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wral 2908
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2913
This theorem is referenced by:  ralcom13  3094  ralrot3  3096  ralcom4  3214  ssint  4465  iinrab2  4556  disjxun  4621  reusv3  4846  cnvpo  5642  cnvso  5643  fununi  5932  isocnv2  6546  dfsmo2  7404  ixpiin  7894  boxriin  7910  dedekind  10160  rexfiuz  14037  gcdcllem1  15164  mreacs  16259  comfeq  16306  catpropd  16309  isnsg2  17564  cntzrec  17706  oppgsubm  17732  opprirred  18642  opprsubrg  18741  rmodislmodlem  18870  rmodislmod  18871  islindf4  20117  cpmatmcllem  20463  tgss2  20731  ist1-2  21091  kgencn  21299  ptcnplem  21364  cnmptcom  21421  fbun  21584  cnflf  21746  fclsopn  21758  cnfcf  21786  isclmp  22837  isncvsngp  22889  caucfil  23021  ovolgelb  23188  dyadmax  23306  ftc1a  23738  ulmcau  24087  perpcom  25542  colinearalg  25724  uhgrvd00  26350  pthdlem2lem  26566  frgrwopreg2  27080  phoeqi  27601  ho02i  28576  hoeq2  28578  adjsym  28580  cnvadj  28639  mddmd2  29056  cdj3lem3b  29187  cvmlift2lem12  31057  dfpo2  31406  elpotr  31440  poimirlem29  33109  heicant  33115  ispsubsp2  34551  ntrclsiso  37886  ntrneiiso  37910  ntrneik2  37911  ntrneix2  37912  ntrneik3  37915  ntrneix3  37916  ntrneik13  37917  ntrneix13  37918  ntrneik4w  37919  hbra2VD  38618  2reu4a  40523
  Copyright terms: Public domain W3C validator