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

Theorem sumeq1d 13162
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 13150 . 2  |-  ( A  =  B  ->  sum_ k  e.  A  C  =  sum_ k  e.  B  C
)
31, 2syl 16 1  |-  ( ph  -> 
sum_ k  e.  A  C  =  sum_ k  e.  B  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1362   sum_csu 13147
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-opab 4339  df-mpt 4340  df-cnv 4835  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840  df-iota 5369  df-f 5410  df-f1 5411  df-fo 5412  df-f1o 5413  df-fv 5414  df-ov 6083  df-oprab 6084  df-mpt2 6085  df-recs 6818  df-rdg 6852  df-seq 11791  df-sum 13148
This theorem is referenced by:  sumeq12dv  13167  sumeq12rdv  13168  fsumf1o  13184  sumss  13185  fsumcllem  13193  fsum1  13202  fzosump1  13205  fsump1  13207  fsum2d  13222  fsumcom2  13225  fsumshftm  13231  fsumrev2  13232  fsumtscopo  13248  fsumtscop  13250  fsumtscop2  13251  fsumparts  13252  fsumiun  13267  bcxmas  13281  incexclem  13282  incexc2  13284  isumsplit  13286  isum1p  13287  arisum  13305  arisum2  13306  geoser  13312  geolim  13313  geo2sum2  13317  mertenslem1  13327  mertenslem2  13328  mertens  13329  efcvgfsum  13354  eftlub  13376  effsumlt  13378  eirrlem  13469  bitsinv1  13621  bitsinvp1  13628  pcfac  13944  prmreclem4  13963  prmreclem6  13965  ovoliunlem1  20827  uniioombllem3  20907  itg11  21011  dvfsumlem1  21340  dvfsumlem4  21343  dvfsum2  21348  elplyr  21554  coeeu  21578  coeeq  21580  plyco  21594  0dgrb  21599  dvply2g  21636  vieta1lem2  21662  vieta1  21663  aaliou3lem5  21698  aaliou3lem6  21699  aaliou3lem7  21700  taylpfval  21715  pserdvlem2  21778  abelthlem6  21786  logfac  21934  advlogexp  21985  emcllem2  22275  emcllem3  22276  emcllem7  22280  harmonicbnd  22282  harmonicbnd2  22283  harmonicbnd3  22286  harmonicbnd4  22289  chtval  22333  chpval  22345  chtfl  22372  chpfl  22373  chtprm  22376  chtnprm  22377  chpp1  22378  chtdif  22381  prmorcht  22401  musum  22416  muinv  22418  logfaclbnd  22446  logfacbnd3  22447  logexprlim  22449  chtppilimlem1  22607  rplogsumlem2  22619  rpvmasumlem  22621  dchrisumlem1  22623  dchrisumlem2  22624  dchrisumlem3  22625  dchrisum  22626  dchrisum0fval  22639  dchrisum0ff  22641  dchrisum0flblem1  22642  dchrisum0lem2  22652  dchrisum0  22654  mulog2sumlem1  22668  2vmadivsumlem  22674  log2sumbnd  22678  logdivbnd  22690  selberg3lem1  22691  pntrsumbnd  22700  pntrsumbnd2  22701  pntrlog2bndlem1  22711  pntrlog2bndlem4  22714  pntpbnd1  22720  pntpbnd2  22721  pntlemf  22739  brcgr  22969  axlowdimlem16  23026  eengv  23048  eulerpartlemgs2  26611  signsvfn  26831  subfacval2  26923  subfaclim  26924  fprodefsum  27332  bpolydiflem  28044  mettrifi  28497  rrncmslem  28575  stoweidlem17  29658  stoweidlem20  29661  stirlinglem12  29726
  Copyright terms: Public domain W3C validator