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

Theorem sumeq1d 12174
Description: Equality deduction for sum. (Contributed by NM, 1-Nov-2005.)
Hypothesis
Ref Expression
sumeq1d.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
sumeq1d  |-  ( ph  -> 
sum_ k  e.  A  C  =  sum_ k  e.  B  C )
Distinct variable groups:    A, k    B, k
Allowed substitution hints:    ph( k)    C( k)

Proof of Theorem sumeq1d
StepHypRef Expression
1 sumeq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 sumeq1 12162 . 2  |-  ( A  =  B  ->  sum_ k  e.  A  C  =  sum_ k  e.  B  C
)
31, 2syl 15 1  |-  ( ph  -> 
sum_ k  e.  A  C  =  sum_ k  e.  B  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623   sum_csu 12158
This theorem is referenced by:  sumeq12dv  12179  sumeq12rdv  12180  fsumf1o  12196  sumss  12197  fsumcllem  12205  fsum1  12214  fzosump1  12217  fsump1  12219  fsum2d  12234  fsumcom2  12237  fsumshftm  12243  fsumrev2  12244  fsumtscopo  12260  fsumtscop  12262  fsumtscop2  12263  fsumparts  12264  fsumiun  12279  bcxmas  12294  incexclem  12295  incexc2  12297  isumsplit  12299  isum1p  12300  arisum  12318  arisum2  12319  geoser  12325  geolim  12326  geo2sum2  12330  mertenslem1  12340  mertenslem2  12341  mertens  12342  efcvgfsum  12367  eftlub  12389  effsumlt  12391  eirrlem  12482  bitsinv1  12633  bitsinvp1  12640  pcfac  12947  prmreclem4  12966  prmreclem6  12968  ovoliunlem1  18861  uniioombllem3  18940  itg11  19046  dvfsumlem1  19373  dvfsumlem4  19376  dvfsum2  19381  elplyr  19583  coeeu  19607  coeeq  19609  plyco  19623  0dgrb  19628  dvply2g  19665  vieta1lem2  19691  vieta1  19692  aaliou3lem5  19727  aaliou3lem6  19728  aaliou3lem7  19729  taylpfval  19744  pserdvlem2  19804  abelthlem6  19812  logfac  19954  advlogexp  20002  emcllem2  20290  emcllem3  20291  emcllem7  20295  harmonicbnd  20297  harmonicbnd2  20298  harmonicbnd3  20301  harmonicbnd4  20304  chtval  20348  chpval  20360  chtfl  20387  chpfl  20388  chtprm  20391  chtnprm  20392  chpp1  20393  chtdif  20396  prmorcht  20416  musum  20431  muinv  20433  logfaclbnd  20461  logfacbnd3  20462  logexprlim  20464  chtppilimlem1  20622  rplogsumlem2  20634  rpvmasumlem  20636  dchrisumlem1  20638  dchrisumlem2  20639  dchrisumlem3  20640  dchrisum  20641  dchrisum0fval  20654  dchrisum0ff  20656  dchrisum0flblem1  20657  dchrisum0lem2  20667  dchrisum0  20669  mulog2sumlem1  20683  2vmadivsumlem  20689  log2sumbnd  20693  logdivbnd  20705  selberg3lem1  20706  pntrsumbnd  20715  pntrsumbnd2  20716  pntrlog2bndlem1  20726  pntrlog2bndlem4  20729  pntpbnd1  20735  pntpbnd2  20736  pntlemf  20754  subfacval2  23718  subfaclim  23719  brcgr  24528  axlowdimlem16  24585  bpolydiflem  24789  mettrifi  26473  rrncmslem  26556  stoweidlem17  27766  stoweidlem20  27769  stirlinglem12  27834
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-opab 4078  df-mpt 4079  df-cnv 4697  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263  df-ov 5861  df-oprab 5862  df-mpt2 5863  df-recs 6388  df-rdg 6423  df-seq 11047  df-sum 12159
  Copyright terms: Public domain W3C validator