Theorem sumeq1i 15055

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 15045	. 2 ⊢ (𝐴 = 𝐵 → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐶)
3	1, 2	ax-mp 5	1 ⊢ Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐶

Syntax hints:   = wceq 1537  Σcsu 15042

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-mpt 5147  df-xp 5561  df-cnv 5563  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-pred 6148  df-iota 6314  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-ov 7159  df-oprab 7160  df-mpo 7161  df-wrecs 7947  df-recs 8008  df-rdg 8046  df-seq 13371  df-sum 15043

This theorem is referenced by:  sumeq12i  15057  fsump1i  15124  fsum2d  15126  fsumxp  15127  isumnn0nn  15197  arisum  15215  arisum2  15216  geo2sum  15229  bpoly0  15404  bpoly1  15405  bpoly2  15411  bpoly3  15412  bpoly4  15413  efsep  15463  ef4p  15466  rpnnen2lem12  15578  ovolicc2lem4  24121  itg10  24289  dveflem  24576  dvply1  24873  vieta1lem2  24900  aaliou3lem4  24935  dvtaylp  24958  pserdvlem2  25016  advlogexp  25238  log2ublem2  25525  log2ublem3  25526  log2ub  25527  ftalem5  25654  cht1  25742  1sgmprm  25775  lgsquadlem2  25957  axlowdimlem16  26743  finsumvtxdg2ssteplem4  27330  rusgrnumwwlks  27753  signsvf0  31850  signsvf1  31851  repr0  31882  k0004val0  40524  binomcxplemnotnn0  40708  fsumiunss  41876  dvnmul  42248  stoweidlem17  42322  dirkertrigeqlem1  42403  etransclem24  42563  etransclem35  42574