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

Theorem ralcom 2972
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 2646 . 2 𝑦𝐴
2 nfcv 2646 . 2 𝑥𝐵
31, 2ralcomf 2970 1 (∀𝑥𝐴𝑦𝐵 𝜑 ↔ ∀𝑦𝐵𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 191  wral 2791
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883  ax-10 1965  ax-11 1970  ax-12 1983  ax-13 2137  ax-ext 2485
This theorem depends on definitions:  df-bi 192  df-or 379  df-an 380  df-ex 1693  df-nf 1697  df-sb 1829  df-cleq 2498  df-clel 2501  df-nfc 2635  df-ral 2796
This theorem is referenced by:  ralcom4  3087  ssint  4280  iinrab2  4370  disjxun  4432  reusv3  4650  cnvpo  5425  cnvso  5426  fununi  5704  isocnv2  6295  dfsmo2  7143  ixpiin  7631  boxriin  7647  dedekind  9882  rexfiuz  13570  gcdcllem1  14635  mreacs  15730  comfeq  15777  catpropd  15780  isnsg2  17007  cntzrec  17148  oppgsubm  17174  opprirred  18090  opprsubrg  18189  islindf4  19554  cpmatmcllem  19900  tgss2  20160  ist1-2  20520  kgencn  20728  ptcnplem  20793  cnmptcom  20850  fbun  21013  cnflf  21175  fclsopn  21187  cnfcf  21215  caucfil  22412  ovolgelb  22592  dyadmax  22716  ftc1a  23150  ulmcau  23511  perpcom  24919  colinearalg  25101  frgrawopreg2  25939  phoeqi  26662  ho02i  27645  hoeq2  27647  adjsym  27649  cnvadj  27708  mddmd2  28125  cdj3lem3b  28256  cvmlift2lem12  30189  dfpo2  30546  elpotr  30578  poimirlem29  32207  heicant  32213  ispsubsp2  33551  ntrclsiso  36885  ntrneiiso  36902  ntrneik2  36903  ntrneix2  36904  hbra2VD  37605  2reu4a  39130  uhgrvd00  40150  pthdlem2lem  40373  frgrwopreg2  40888
  Copyright terms: Public domain W3C validator