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

Theorem ralcom 3127
Description: Commutation of restricted universal quantifiers. See ralcom2 3133 for a version without DV condition on 𝑥, 𝑦. (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 2793 . 2 𝑦𝐴
2 nfcv 2793 . 2 𝑥𝐵
31, 2ralcomf 3125 1 (∀𝑥𝐴𝑦𝐵 𝜑 ↔ ∀𝑦𝐵𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wral 2941
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946
This theorem is referenced by:  ralcom13  3129  ralrot3  3131  ralcom4  3255  ssint  4525  iinrab2  4615  disjxun  4683  reusv3  4906  cnvpo  5711  cnvso  5712  fununi  6002  isocnv2  6621  dfsmo2  7489  ixpiin  7976  boxriin  7992  dedekind  10238  rexfiuz  14131  gcdcllem1  15268  mreacs  16366  comfeq  16413  catpropd  16416  isnsg2  17671  cntzrec  17812  oppgsubm  17838  opprirred  18748  opprsubrg  18849  rmodislmodlem  18978  rmodislmod  18979  islindf4  20225  cpmatmcllem  20571  tgss2  20839  ist1-2  21199  kgencn  21407  ptcnplem  21472  cnmptcom  21529  fbun  21691  cnflf  21853  fclsopn  21865  cnfcf  21893  isclmp  22943  isncvsngp  22995  caucfil  23127  ovolgelb  23294  dyadmax  23412  ftc1a  23845  ulmcau  24194  perpcom  25653  colinearalg  25835  uhgrvd00  26486  pthdlem2lem  26719  frgrwopregbsn  27297  phoeqi  27841  ho02i  28816  hoeq2  28818  adjsym  28820  cnvadj  28879  mddmd2  29296  cdj3lem3b  29427  cvmlift2lem12  31422  dfpo2  31771  elpotr  31810  noetalem3  31990  conway  32035  poimirlem29  33568  heicant  33574  ispsubsp2  35350  ntrclsiso  38682  ntrneiiso  38706  ntrneik2  38707  ntrneix2  38708  ntrneik3  38711  ntrneix3  38712  ntrneik13  38713  ntrneix13  38714  ntrneik4w  38715  hbra2VD  39410  2reu4a  41510
  Copyright terms: Public domain W3C validator