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

Theorem sumeq1i 15588
Description: Equality inference for sum. (Contributed by NM, 2-Jan-2006.)
Hypothesis
Ref Expression
sumeq1i.1 𝐴 = 𝐵
Assertion
Ref Expression
sumeq1i Σ𝑘𝐴 𝐶 = Σ𝑘𝐵 𝐶
Distinct variable groups:   𝐴,𝑘   𝐵,𝑘
Allowed substitution hint:   𝐶(𝑘)

Proof of Theorem sumeq1i
StepHypRef Expression
1 sumeq1i.1 . 2 𝐴 = 𝐵
2 sumeq1 15579 . 2 (𝐴 = 𝐵 → Σ𝑘𝐴 𝐶 = Σ𝑘𝐵 𝐶)
31, 2ax-mp 5 1 Σ𝑘𝐴 𝐶 = Σ𝑘𝐵 𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  Σcsu 15576
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3062  df-rex 3071  df-rab 3407  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-opab 5169  df-mpt 5190  df-xp 5640  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6254  df-iota 6449  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-ov 7361  df-oprab 7362  df-mpo 7363  df-frecs 8213  df-wrecs 8244  df-recs 8318  df-rdg 8357  df-seq 13913  df-sum 15577
This theorem is referenced by:  sumeq12i  15590  fsump1i  15659  fsum2d  15661  fsumxp  15662  isumnn0nn  15732  arisum  15750  arisum2  15751  geo2sum  15763  bpoly0  15938  bpoly1  15939  bpoly2  15945  bpoly3  15946  bpoly4  15947  efsep  15997  ef4p  16000  rpnnen2lem12  16112  ovolicc2lem4  24900  itg10  25068  dveflem  25359  dvply1  25660  vieta1lem2  25687  aaliou3lem4  25722  dvtaylp  25745  pserdvlem2  25803  advlogexp  26026  log2ublem2  26313  log2ublem3  26314  log2ub  26315  ftalem5  26442  cht1  26530  1sgmprm  26563  lgsquadlem2  26745  axlowdimlem16  27948  finsumvtxdg2ssteplem4  28538  rusgrnumwwlks  28961  signsvf0  33249  signsvf1  33250  repr0  33281  k0004val0  42514  binomcxplemnotnn0  42724  fsumiunss  43902  dvnmul  44270  stoweidlem17  44344  dirkertrigeqlem1  44425  etransclem24  44585  etransclem35  44596
  Copyright terms: Public domain W3C validator