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

Theorem raleq 3032
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 2591 . 2  |-  F/_ x A
2 nfcv 2591 . 2  |-  F/_ x B
31, 2raleqf 3028 1  |-  ( A  =  B  ->  ( A. x  e.  A  ph  <->  A. x  e.  B  ph ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    = wceq 1437   A.wral 2782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ral 2787
This theorem is referenced by:  raleqi  3036  raleqdv  3038  raleqbi1dv  3040  sbralie  3075  r19.2zb  3893  inteq  4261  iineq1  4317  fri  4816  frsn  4925  fncnv  5665  isoeq4  6228  onminex  6648  tfinds  6700  f1oweALT  6791  frxp  6917  wfrlem1  7043  wfrlem15  7058  tfrlem1  7102  tfrlem12  7115  omeulem1  7291  ixpeq1  7541  undifixp  7566  ac6sfi  7821  frfi  7822  iunfi  7868  indexfi  7888  supeq1  7965  supeq2  7968  bnd2  8363  acneq  8472  aceq3lem  8549  dfac5lem4  8555  dfac8  8563  dfac9  8564  kmlem1  8578  kmlem10  8587  kmlem13  8590  cfval  8675  axcc2lem  8864  axcc4dom  8869  axdc3lem3  8880  axdc3lem4  8881  ac4c  8904  ac5  8905  ac6sg  8916  zorn2lem7  8930  xrsupsslem  11592  xrinfmsslem  11593  xrsupss  11594  xrinfmss  11595  fsuppmapnn0fiubex  12201  rexanuz  13387  rexfiuz  13389  modfsummod  13832  gcdcllem3  14449  lcmfval  14562  lcmf0val  14563  lcmfvalOLD  14566  lcmfunsnlem  14585  coprmprod  14649  coprmproddvds  14651  isprs  16126  drsdirfi  16134  isdrs2  16135  ispos  16143  lubeldm  16178  lubval  16181  glbeldm  16191  glbval  16194  istos  16232  pospropd  16331  isdlat  16390  mhmpropd  16539  isghm  16834  cntzval  16926  efgval  17302  iscmn  17372  dfrhm2  17880  lidldvgen  18414  coe1fzgsumd  18831  evl1gsumd  18880  ocvval  19161  isobs  19214  mat0dimcrng  19426  mdetunilem9  19576  ist0  20267  cmpcovf  20337  is1stc  20387  2ndc1stc  20397  isref  20455  txflf  20952  ustuqtop4  21190  iscfilu  21234  ispsmet  21251  ismet  21269  isxmet  21270  cncfval  21816  lebnumlem3  21887  fmcfil  22135  iscfil3  22136  caucfil  22146  iscmet3  22156  cfilres  22159  minveclem3  22264  ovolfiniun  22332  finiunmbl  22374  volfiniun  22377  dvcn  22752  ulmval  23200  axtgcont1  24379  nb3grapr  25026  rusgrasn  25518  isplig  25754  isgrpo  25769  isablo  25856  isexid2  25898  ismndo2  25918  rngomndo  25994  ocval  26768  acunirnmpt  28101  isomnd  28302  isorng  28401  ismbfm  28913  isanmbfm  28917  bnj865  29522  bnj1154  29596  bnj1296  29618  bnj1463  29652  derangval  29678  setinds  30211  dfon2lem3  30218  dfon2lem7  30222  tfisg  30244  poseq  30278  frrlem1  30301  sltval2  30330  sltres  30338  nodense  30363  nobndup  30374  nobnddown  30375  nofulllem1  30376  dfrecs2  30502  dfrdg4  30503  isfne  30780  finixpnum  31634  mblfinlem1  31681  mbfresfi  31691  indexdom  31765  heibor1lem  31845  pridl  31974  smprngopr  31989  ispridlc  32007  setindtrs  35586  dford3lem2  35588  dfac11  35626  fnchoice  36990  stoweidlem31  37461  stoweidlem57  37487  fourierdlem80  37618  fourierdlem103  37641  fourierdlem104  37642  issal  37722  mgmhmpropd  38543  rnghmval  38649  zrrnghm  38675
  Copyright terms: Public domain W3C validator