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

Theorem ralcom 3246
Description: Commutation of restricted universal quantifiers. See ralcom2 3252 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 2913 . 2 𝑦𝐴
2 nfcv 2913 . 2 𝑥𝐵
31, 2ralcomf 3244 1 (∀𝑥𝐴𝑦𝐵 𝜑 ↔ ∀𝑦𝐵𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wral 3061
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clel 2767  df-nfc 2902  df-ral 3066
This theorem is referenced by:  ralcom13  3248  ralrot3  3250  ralcom4  3376  ssint  4628  iinrab2  4718  disjxun  4785  reusv3  5006  cnvpo  5818  cnvso  5819  fununi  6105  isocnv2  6725  dfsmo2  7598  ixpiin  8089  boxriin  8105  dedekind  10403  rexfiuz  14296  gcdcllem1  15430  mreacs  16527  comfeq  16574  catpropd  16577  isnsg2  17833  cntzrec  17974  oppgsubm  18000  opprirred  18911  opprsubrg  19012  rmodislmodlem  19141  rmodislmod  19142  islindf4  20395  cpmatmcllem  20744  tgss2  21013  ist1-2  21373  kgencn  21581  ptcnplem  21646  cnmptcom  21703  fbun  21865  cnflf  22027  fclsopn  22039  cnfcf  22067  isclmp  23117  isncvsngp  23169  caucfil  23301  ovolgelb  23469  dyadmax  23587  ftc1a  24021  ulmcau  24370  perpcom  25830  colinearalg  26012  uhgrvd00  26666  pthdlem2lem  26899  frgrwopregbsn  27500  phoeqi  28054  ho02i  29029  hoeq2  29031  adjsym  29033  cnvadj  29092  mddmd2  29509  cdj3lem3b  29640  cvmlift2lem12  31635  dfpo2  31984  elpotr  32023  noetalem3  32203  conway  32248  poimirlem29  33772  heicant  33778  ispsubsp2  35555  ntrclsiso  38892  ntrneiiso  38916  ntrneik2  38917  ntrneix2  38918  ntrneik3  38921  ntrneix3  38922  ntrneik13  38923  ntrneix13  38924  ntrneik4w  38925  hbra2VD  39619  2reu4a  41710
  Copyright terms: Public domain W3C validator