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

Theorem raleq 2864
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 2540 . 2  |-  F/_ x A
2 nfcv 2540 . 2  |-  F/_ x B
31, 2raleqf 2860 1  |-  ( A  =  B  ->  ( A. x  e.  A  ph  <->  A. x  e.  B  ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1649   A.wral 2666
This theorem is referenced by:  raleqi  2868  raleqdv  2870  raleqbi1dv  2872  sbralie  2905  r19.2zb  3678  inteq  4013  iineq1  4067  fri  4504  reusv6OLD  4693  reusv7OLD  4694  onminex  4746  tfinds  4798  frsn  4907  fncnv  5474  isoeq4  6001  f1oweALT  6033  frxp  6415  tfrlem1  6595  tfrlem3  6597  tfrlem12  6609  omeulem1  6784  ixpeq1  7032  undifixp  7057  ac6sfi  7310  frfi  7311  iunfi  7353  indexfi  7372  supeq1  7408  supeq2  7411  bnd2  7773  acneq  7880  aceq3lem  7957  dfac5lem4  7963  dfac8  7971  dfac9  7972  kmlem1  7986  kmlem10  7995  kmlem13  7998  cfval  8083  axcc2lem  8272  axcc4dom  8277  axdc3lem3  8288  axdc3lem4  8289  ac4c  8312  ac5  8313  ac6sg  8324  zorn2lem7  8338  xrsupsslem  10841  xrinfmsslem  10842  xrsupss  10843  xrinfmss  10844  rexanuz  12104  rexfiuz  12106  gcdcllem3  12968  isprs  14342  drsdirfi  14350  isdrs2  14351  ispos  14359  lubval  14391  glbval  14396  istos  14419  pospropd  14516  isdlat  14574  spwval2  14611  spwpr2  14615  mhmpropd  14699  isghm  14961  cntzval  15075  efgval  15304  iscmn  15374  dfrhm2  15776  lidldvgen  16281  ocvval  16849  isobs  16902  ist0  17338  cmpcovf  17408  is1stc  17457  2ndc1stc  17467  txflf  17991  ustuqtop4  18227  iscfilu  18271  ispsmet  18288  ismet  18306  isxmet  18307  cncfval  18871  lebnumlem3  18941  fmcfil  19178  iscfil3  19179  caucfil  19189  iscmet3  19199  cfilres  19202  minveclem3  19283  ovolfiniun  19350  finiunmbl  19391  volfiniun  19394  dvcn  19760  ulmval  20249  nb3grapr  21415  isplig  21718  isgrpo  21737  isablo  21824  isexid2  21866  ismndo2  21886  rngomndo  21962  ocval  22735  isofld  24188  ismbfm  24555  isanmbfm  24559  derangval  24806  setinds  25348  dfon2lem3  25355  dfon2lem7  25359  tfisg  25418  poseq  25467  wfrlem1  25470  wfrlem15  25484  frrlem1  25495  sltval2  25524  sltres  25532  nodense  25557  nobndup  25568  nobnddown  25569  nofulllem1  25570  dfrdg4  25703  tfrqfree  25704  bpolyval  25999  mblfinlem  26143  mbfresfi  26152  isfne  26238  isref  26249  indexdom  26326  heibor1lem  26408  pridl  26537  smprngopr  26552  ispridlc  26570  setindtrs  26986  dford3lem2  26988  dfac11  27028  fnchoice  27567  stoweidlem31  27647  stoweidlem57  27673  bnj865  29000  bnj1154  29074  bnj1296  29096  bnj1463  29130
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ral 2671
  Copyright terms: Public domain W3C validator