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

Theorem raleq 2749
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 2432 . 2  |-  F/_ x A
2 nfcv 2432 . 2  |-  F/_ x B
31, 2raleqf 2745 1  |-  ( A  =  B  ->  ( A. x  e.  A  ph  <->  A. x  e.  B  ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1632   A.wral 2556
This theorem is referenced by:  raleqi  2753  raleqdv  2755  raleqbi1dv  2757  sbralie  2790  r19.2zb  3557  inteq  3881  iineq1  3935  fri  4371  reusv6OLD  4561  reusv7OLD  4562  onminex  4614  tfinds  4666  frsn  4776  fncnv  5330  isoeq4  5835  f1oweALT  5867  frxp  6241  tfrlem1  6407  tfrlem3  6409  tfrlem12  6421  omeulem1  6596  ixpeq1  6843  undifixp  6868  ac6sfi  7117  frfi  7118  iunfi  7160  indexfi  7179  supeq1  7214  supeq2  7217  bnd2  7579  acneq  7686  aceq3lem  7763  dfac5lem4  7769  dfac8  7777  dfac9  7778  kmlem1  7792  kmlem10  7801  kmlem13  7804  cfval  7889  axcc2lem  8078  axcc4dom  8083  axdc3lem3  8094  axdc3lem4  8095  ac4c  8119  ac5  8120  ac6sg  8131  zorn2lem7  8145  xrsupsslem  10641  xrinfmsslem  10642  xrsupss  10643  xrinfmss  10644  rexanuz  11845  rexfiuz  11847  gcdcllem3  12708  isprs  14080  drsdirfi  14088  isdrs2  14089  ispos  14097  lubval  14129  glbval  14134  istos  14157  pospropd  14254  isdlat  14312  spwval2  14349  spwpr2  14353  mhmpropd  14437  isghm  14699  cntzval  14813  efgval  15042  iscmn  15112  dfrhm2  15514  lidldvgen  16023  ocvval  16583  isobs  16636  ist0  17064  cmpcovf  17134  is1stc  17183  2ndc1stc  17193  txflf  17717  ismet  17904  isxmet  17905  cncfval  18408  lebnumlem3  18477  fmcfil  18714  iscfil3  18715  caucfil  18725  iscmet3  18735  cfilres  18738  minveclem3  18809  ovolfiniun  18876  finiunmbl  18917  volfiniun  18920  dvcn  19286  ulmval  19775  isplig  20860  isgrpo  20879  isablo  20966  isexid2  21008  ismndo2  21028  rngomndo  21104  ocval  21875  prsiga  23507  ismbfm  23572  isanmbfm  23576  derangval  23713  setinds  24205  dfon2lem3  24212  dfon2lem7  24216  tfisg  24275  poseq  24324  wfrlem1  24327  wfrlem15  24341  frrlem1  24352  sltval2  24381  sltres  24389  nodense  24414  nobndup  24425  nobnddown  24426  nofulllem1  24427  dfrdg4  24560  tfrqfree  24561  bpolyval  24856  hfext  24885  ac5g  25178  prjmapcp2  25273  islatalg  25286  ubos  25359  defse3  25375  ablocomgrp  25445  com2i  25519  ununr  25523  lvsovso  25729  tcnvec  25793  isibg2  26213  isfne  26371  isref  26382  indexdom  26516  heibor1lem  26636  pridl  26765  smprngopr  26780  ispridlc  26798  setindtrs  27221  dford3lem2  27223  dfac11  27263  fnchoice  27803  stoweidlem31  27883  stoweidlem57  27909  nb3grapr  28289  cusgra3v  28299  bnj865  29271  bnj1154  29345  bnj1296  29367  bnj1463  29401
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ral 2561
  Copyright terms: Public domain W3C validator