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

Theorem sumeq1i 13486
Description: Equality inference for sum. (Contributed by NM, 2-Jan-2006.)
Hypothesis
Ref Expression
sumeq1i.1  |-  A  =  B
Assertion
Ref Expression
sumeq1i  |-  sum_ k  e.  A  C  =  sum_ k  e.  B  C
Distinct variable groups:    A, k    B, k
Allowed substitution hint:    C( k)

Proof of Theorem sumeq1i
StepHypRef Expression
1 sumeq1i.1 . 2  |-  A  =  B
2 sumeq1 13477 . 2  |-  ( A  =  B  ->  sum_ k  e.  A  C  =  sum_ k  e.  B  C
)
31, 2ax-mp 5 1  |-  sum_ k  e.  A  C  =  sum_ k  e.  B  C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1379   sum_csu 13474
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-opab 4506  df-mpt 4507  df-cnv 5007  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5551  df-f 5592  df-f1 5593  df-fo 5594  df-f1o 5595  df-fv 5596  df-ov 6288  df-oprab 6289  df-mpt2 6290  df-recs 7043  df-rdg 7077  df-seq 12077  df-sum 13475
This theorem is referenced by:  sumeq12i  13488  fsump1i  13550  fsum2d  13552  fsumxp  13553  isumnn0nn  13620  arisum  13637  arisum2  13638  geo2sum  13648  efsep  13709  ef4p  13712  rpnnen2  13823  ovolicc2lem4  21758  itg10  21922  dveflem  22207  dvply1  22506  vieta1lem2  22533  aaliou3lem4  22568  dvtaylp  22591  pserdvlem2  22649  advlogexp  22861  log2ublem2  23103  log2ublem3  23104  log2ub  23105  ftalem5  23175  cht1  23264  1sgmprm  23299  lgsquadlem2  23455  axlowdimlem16  24033  rusgranumwlks  24729  signsvf0  28288  signsvf1  28289  bpoly0  29665  bpoly1  29666  bpoly2  29672  bpoly3  29673  bpoly4  29674  stoweidlem17  31544  dirkertrigeqlem1  31625
  Copyright terms: Public domain W3C validator