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

Theorem ralcom 3095
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 2767 . 2 𝑦𝐴
2 nfcv 2767 . 2 𝑥𝐵
31, 2ralcomf 3093 1 (∀𝑥𝐴𝑦𝐵 𝜑 ↔ ∀𝑦𝐵𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wral 2912
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 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606
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 1883  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ral 2917
This theorem is referenced by:  ralcom4  3215  ssint  4463  iinrab2  4554  disjxun  4616  reusv3  4841  cnvpo  5635  cnvso  5636  fununi  5924  isocnv2  6536  dfsmo2  7390  ixpiin  7879  boxriin  7895  dedekind  10145  rexfiuz  14016  gcdcllem1  15140  mreacs  16235  comfeq  16282  catpropd  16285  isnsg2  17540  cntzrec  17682  oppgsubm  17708  opprirred  18618  opprsubrg  18717  islindf4  20091  cpmatmcllem  20437  tgss2  20697  ist1-2  21056  kgencn  21264  ptcnplem  21329  cnmptcom  21386  fbun  21549  cnflf  21711  fclsopn  21723  cnfcf  21751  isclmp  22800  isncvsngp  22852  caucfil  22984  ovolgelb  23150  dyadmax  23267  ftc1a  23699  ulmcau  24048  perpcom  25503  colinearalg  25685  uhgrvd00  26310  pthdlem2lem  26526  frgrwopreg2  27040  phoeqi  27553  ho02i  28528  hoeq2  28530  adjsym  28532  cnvadj  28591  mddmd2  29008  cdj3lem3b  29139  cvmlift2lem12  30996  dfpo2  31344  elpotr  31375  poimirlem29  33037  heicant  33043  ispsubsp2  34479  ntrclsiso  37814  ntrneiiso  37838  ntrneik2  37839  ntrneix2  37840  ntrneik3  37843  ntrneix3  37844  ntrneik13  37845  ntrneix13  37846  ntrneik4w  37847  hbra2VD  38546  2reu4a  40461
  Copyright terms: Public domain W3C validator