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

Theorem raleq 3133
Description: Equality theorem for restricted universal quantifier. (Contributed by NM, 16-Nov-1995.)
Assertion
Ref Expression
raleq (𝐴 = 𝐵 → (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐵 𝜑))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem raleq
StepHypRef Expression
1 nfcv 2762 . 2 𝑥𝐴
2 nfcv 2762 . 2 𝑥𝐵
31, 2raleqf 3129 1 (𝐴 = 𝐵 → (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐵 𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1481  wral 2909
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ral 2914
This theorem is referenced by:  raleqi  3137  raleqdv  3139  raleqbi1dv  3141  sbralie  3179  r19.2zb  4052  inteq  4469  iineq1  4526  fri  5066  frsn  5179  fncnv  5950  isoeq4  6555  onminex  6992  tfinds  7044  f1oweALT  7137  frxp  7272  wfrlem1  7399  wfrlem15  7414  tfrlem1  7457  tfrlem12  7470  omeulem1  7647  ixpeq1  7904  undifixp  7929  ac6sfi  8189  frfi  8190  iunfi  8239  indexfi  8259  supeq1  8336  supeq2  8339  bnd2  8741  acneq  8851  aceq3lem  8928  dfac5lem4  8934  dfac8  8942  dfac9  8943  kmlem1  8957  kmlem10  8966  kmlem13  8969  cfval  9054  axcc2lem  9243  axcc4dom  9248  axdc3lem3  9259  axdc3lem4  9260  ac4c  9283  ac5  9284  ac6sg  9295  zorn2lem7  9309  xrsupsslem  12122  xrinfmsslem  12123  xrsupss  12124  xrinfmss  12125  fsuppmapnn0fiubex  12775  rexanuz  14066  rexfiuz  14068  modfsummod  14507  gcdcllem3  15204  lcmfval  15315  lcmf0val  15316  lcmfunsnlem  15335  coprmprod  15356  coprmproddvds  15358  isprs  16911  drsdirfi  16919  isdrs2  16920  ispos  16928  lubeldm  16962  lubval  16965  glbeldm  16975  glbval  16978  istos  17016  pospropd  17115  isdlat  17174  mhmpropd  17322  isghm  17641  cntzval  17735  efgval  18111  iscmn  18181  dfrhm2  18698  lidldvgen  19236  coe1fzgsumd  19653  evl1gsumd  19702  ocvval  19992  isobs  20045  mat0dimcrng  20257  mdetunilem9  20407  ist0  21105  cmpcovf  21175  is1stc  21225  2ndc1stc  21235  isref  21293  txflf  21791  ustuqtop4  22029  iscfilu  22073  ispsmet  22090  ismet  22109  isxmet  22110  cncfval  22672  lebnumlem3  22743  fmcfil  23051  iscfil3  23052  caucfil  23062  iscmet3  23072  cfilres  23075  minveclem3  23181  ovolfiniun  23250  finiunmbl  23293  volfiniun  23296  dvcn  23665  ulmval  24115  axtgcont1  25348  tgcgr4  25407  nb3grpr  26265  dfconngr1  27028  isconngr  27029  1conngr  27034  frgr0v  27105  isplig  27298  isgrpo  27321  isablo  27370  ocval  28109  acunirnmpt  29432  isomnd  29675  isorng  29773  ismbfm  30288  isanmbfm  30292  bnj865  30967  bnj1154  31041  bnj1296  31063  bnj1463  31097  derangval  31123  setinds  31657  dfon2lem3  31664  dfon2lem7  31668  tfisg  31690  poseq  31724  frrlem1  31754  sltval2  31783  sltres  31789  nolesgn2o  31798  nodense  31816  nosupbnd2lem1  31835  brsslt  31874  dfrecs2  32032  dfrdg4  32033  isfne  32309  finixpnum  33365  mblfinlem1  33417  mbfresfi  33427  indexdom  33500  heibor1lem  33579  isexid2  33625  ismndo2  33644  rngomndo  33705  pridl  33807  smprngopr  33822  ispridlc  33840  setindtrs  37411  dford3lem2  37413  dfac11  37451  fnchoice  39008  axccdom  39232  axccd  39245  stoweidlem31  40011  stoweidlem57  40037  fourierdlem80  40166  fourierdlem103  40189  fourierdlem104  40190  isvonmbl  40615  mgmhmpropd  41550  rnghmval  41656  zrrnghm  41682  bnd2d  42193
  Copyright terms: Public domain W3C validator