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

Theorem sumeq1i 14671
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 14662 . 2 (𝐴 = 𝐵 → Σ𝑘𝐴 𝐶 = Σ𝑘𝐵 𝐶)
31, 2ax-mp 5 1 Σ𝑘𝐴 𝐶 = Σ𝑘𝐵 𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1637  Σcsu 14659
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ral 3112  df-rex 3113  df-rab 3116  df-v 3404  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-nul 4128  df-if 4291  df-sn 4382  df-pr 4384  df-op 4388  df-uni 4642  df-br 4856  df-opab 4918  df-mpt 4935  df-xp 5330  df-cnv 5332  df-dm 5334  df-rn 5335  df-res 5336  df-ima 5337  df-pred 5907  df-iota 6074  df-f 6115  df-f1 6116  df-fo 6117  df-f1o 6118  df-fv 6119  df-ov 6887  df-oprab 6888  df-mpt2 6889  df-wrecs 7652  df-recs 7714  df-rdg 7752  df-seq 13045  df-sum 14660
This theorem is referenced by:  sumeq12i  14673  fsump1i  14743  fsum2d  14745  fsumxp  14746  isumnn0nn  14816  arisum  14834  arisum2  14835  geo2sum  14846  bpoly0  15021  bpoly1  15022  bpoly2  15028  bpoly3  15029  bpoly4  15030  efsep  15080  ef4p  15083  rpnnen2lem12  15194  ovolicc2lem4  23524  itg10  23692  dveflem  23979  dvply1  24276  vieta1lem2  24303  aaliou3lem4  24338  dvtaylp  24361  pserdvlem2  24419  advlogexp  24638  log2ublem2  24911  log2ublem3  24912  log2ub  24913  ftalem5  25040  cht1  25128  1sgmprm  25161  lgsquadlem2  25343  axlowdimlem16  26074  finsumvtxdg2ssteplem4  26695  rusgrnumwwlks  27139  signsvf0  31005  signsvf1  31006  repr0  31037  k0004val0  38970  binomcxplemnotnn0  39073  fsumiunss  40305  dvnmul  40656  stoweidlem17  40731  dirkertrigeqlem1  40812  etransclem24  40972  etransclem35  40983
  Copyright terms: Public domain W3C validator