Theorem sumeq1i 15648

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

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

Syntax hints:   = wceq 1539  Σcsu 15636

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-xp 5681  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6299  df-iota 6494  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-ov 7414  df-oprab 7415  df-mpo 7416  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-seq 13971  df-sum 15637

This theorem is referenced by:  sumeq12i  15650  fsump1i  15719  fsum2d  15721  fsumxp  15722  isumnn0nn  15792  arisum  15810  arisum2  15811  geo2sum  15823  bpoly0  15998  bpoly1  15999  bpoly2  16005  bpoly3  16006  bpoly4  16007  efsep  16057  ef4p  16060  rpnnen2lem12  16172  ovolicc2lem4  25269  itg10  25437  dveflem  25731  dvply1  26033  vieta1lem2  26060  aaliou3lem4  26095  dvtaylp  26118  pserdvlem2  26176  advlogexp  26399  log2ublem2  26688  log2ublem3  26689  log2ub  26690  ftalem5  26817  cht1  26905  1sgmprm  26938  lgsquadlem2  27120  axlowdimlem16  28482  finsumvtxdg2ssteplem4  29072  rusgrnumwwlks  29495  signsvf0  33889  signsvf1  33890  repr0  33921  sumcubes  41513  k0004val0  43207  binomcxplemnotnn0  43417  fsumiunss  44589  dvnmul  44957  stoweidlem17  45031  dirkertrigeqlem1  45112  etransclem24  45272  etransclem35  45283