Theorem sumeq1i 15618

Description: Equality inference for sum. (Contributed by NM, 2-Jan-2006.)

Hypothesis

Ref	Expression
sumeq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
sumeq1i	⊢ Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐶

Proof of Theorem sumeq1i

Step	Hyp	Ref	Expression
1		sumeq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		sumeq1 15610	. 2 ⊢ (𝐴 = 𝐵 → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐶)
3	1, 2	ax-mp 5	1 ⊢ Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐶

Syntax hints:   = wceq 1541  Σcsu 15607

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-mpt 5178  df-xp 5628  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-pred 6257  df-iota 6446  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-ov 7359  df-oprab 7360  df-mpo 7361  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-seq 13923  df-sum 15608

This theorem is referenced by:  sumeq12i  15620  fsump1i  15690  fsum2d  15692  fsumxp  15693  isumnn0nn  15763  arisum  15781  arisum2  15782  geo2sum  15794  bpoly0  15971  bpoly1  15972  bpoly2  15978  bpoly3  15979  bpoly4  15980  efsep  16033  ef4p  16036  rpnnen2lem12  16148  ovolicc2lem4  25475  itg10  25643  dveflem  25937  dvply1  26245  vieta1lem2  26273  aaliou3lem4  26308  dvtaylp  26332  pserdvlem2  26392  advlogexp  26618  log2ublem2  26911  log2ublem3  26912  log2ub  26913  ftalem5  27041  cht1  27129  1sgmprm  27164  lgsquadlem2  27346  axlowdimlem16  28979  finsumvtxdg2ssteplem4  29571  rusgrnumwwlks  29999  cos9thpiminplylem3  33890  signsvf0  34686  signsvf1  34687  repr0  34717  sumeq12si  36346  cbvsumvw2  36389  sumcubes  42510  k0004val0  44337  binomcxplemnotnn0  44539  fsumiunss  45763  dvnmul  46129  stoweidlem17  46203  dirkertrigeqlem1  46284  etransclem24  46444  etransclem35  46455