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

Theorem raleq 2973
Description: Equality theorem for restricted universal quantifier. (Contributed by NM, 16-Nov-1995.)
Assertion
Ref Expression
raleq  |-  ( A  =  B  ->  ( A. x  e.  A  ph  <->  A. x  e.  B  ph ) )
Distinct variable groups:    x, A    x, B
Allowed substitution hint:    ph( x)

Proof of Theorem raleq
StepHypRef Expression
1 nfcv 2612 . 2  |-  F/_ x A
2 nfcv 2612 . 2  |-  F/_ x B
31, 2raleqf 2969 1  |-  ( A  =  B  ->  ( A. x  e.  A  ph  <->  A. x  e.  B  ph ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    = wceq 1452   A.wral 2756
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ral 2761
This theorem is referenced by:  raleqi  2977  raleqdv  2979  raleqbi1dv  2981  sbralie  3018  r19.2zb  3850  inteq  4229  iineq1  4284  fri  4801  frsn  4910  fncnv  5657  isoeq4  6231  onminex  6653  tfinds  6705  f1oweALT  6796  frxp  6925  wfrlem1  7053  wfrlem15  7068  tfrlem1  7112  tfrlem12  7125  omeulem1  7301  ixpeq1  7551  undifixp  7576  ac6sfi  7833  frfi  7834  iunfi  7880  indexfi  7900  supeq1  7977  supeq2  7980  bnd2  8382  acneq  8492  aceq3lem  8569  dfac5lem4  8575  dfac8  8583  dfac9  8584  kmlem1  8598  kmlem10  8607  kmlem13  8610  cfval  8695  axcc2lem  8884  axcc4dom  8889  axdc3lem3  8900  axdc3lem4  8901  ac4c  8924  ac5  8925  ac6sg  8936  zorn2lem7  8950  xrsupsslem  11617  xrinfmsslem  11618  xrsupss  11619  xrinfmss  11620  fsuppmapnn0fiubex  12242  rexanuz  13485  rexfiuz  13487  modfsummod  13931  gcdcllem3  14554  lcmfval  14670  lcmf0val  14671  lcmfvalOLD  14674  lcmfunsnlem  14693  coprmprod  14757  coprmproddvds  14759  isprs  16253  drsdirfi  16261  isdrs2  16262  ispos  16270  lubeldm  16305  lubval  16308  glbeldm  16318  glbval  16321  istos  16359  pospropd  16458  isdlat  16517  mhmpropd  16666  isghm  16961  cntzval  17053  efgval  17445  iscmn  17515  dfrhm2  18023  lidldvgen  18556  coe1fzgsumd  18973  evl1gsumd  19022  ocvval  19307  isobs  19360  mat0dimcrng  19572  mdetunilem9  19722  ist0  20413  cmpcovf  20483  is1stc  20533  2ndc1stc  20543  isref  20601  txflf  21099  ustuqtop4  21337  iscfilu  21381  ispsmet  21398  ismet  21416  isxmet  21417  cncfval  21998  lebnumlem3  22069  lebnumlem3OLD  22072  fmcfil  22320  iscfil3  22321  caucfil  22331  iscmet3  22341  cfilres  22344  minveclem3  22449  minveclem3OLD  22461  ovolfiniun  22532  finiunmbl  22576  volfiniun  22579  dvcn  22954  ulmval  23414  axtgcont1  24595  tgcgr4  24655  nb3grapr  25260  rusgrasn  25752  isplig  25988  isgrpo  26005  isablo  26092  isexid2  26134  ismndo2  26154  rngomndo  26230  ocval  27014  acunirnmpt  28336  isomnd  28538  isorng  28636  ismbfm  29147  isanmbfm  29151  bnj865  29806  bnj1154  29880  bnj1296  29902  bnj1463  29936  derangval  29962  setinds  30495  dfon2lem3  30502  dfon2lem7  30506  tfisg  30528  poseq  30562  frrlem1  30585  sltval2  30614  sltres  30622  nodense  30649  nobndup  30660  nobnddown  30661  nofulllem1  30662  dfrecs2  30788  dfrdg4  30789  isfne  31066  finixpnum  31994  mblfinlem1  32041  mbfresfi  32051  indexdom  32125  heibor1lem  32205  pridl  32334  smprngopr  32349  ispridlc  32367  setindtrs  35951  dford3lem2  35953  dfac11  35991  fnchoice  37413  stoweidlem31  38004  stoweidlem57  38030  fourierdlem80  38162  fourierdlem103  38185  fourierdlem104  38186  issal  38287  isvonmbl  38578  nb3grpr  39620  cplgr0v  39659  dfconngr1  40102  isconngr  40103  0vconngr  40107  1conngr  40108  mgmhmpropd  40293  rnghmval  40399  zrrnghm  40425
  Copyright terms: Public domain W3C validator