Theorem sumeq1i 15596

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

Syntax hints:   = wceq 1541  Σcsu 15585

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 2112  ax-9 2120  ax-ext 2702

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 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3394  df-v 3436  df-dif 3903  df-un 3905  df-in 3907  df-ss 3917  df-nul 4282  df-if 4474  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4858  df-br 5090  df-opab 5152  df-mpt 5171  df-xp 5620  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-pred 6244  df-iota 6433  df-f 6481  df-f1 6482  df-fo 6483  df-f1o 6484  df-fv 6485  df-ov 7344  df-oprab 7345  df-mpo 7346  df-frecs 8206  df-wrecs 8237  df-recs 8286  df-rdg 8324  df-seq 13901  df-sum 15586

This theorem is referenced by:  sumeq12i  15598  fsump1i  15668  fsum2d  15670  fsumxp  15671  isumnn0nn  15741  arisum  15759  arisum2  15760  geo2sum  15772  bpoly0  15949  bpoly1  15950  bpoly2  15956  bpoly3  15957  bpoly4  15958  efsep  16011  ef4p  16014  rpnnen2lem12  16126  ovolicc2lem4  25441  itg10  25609  dveflem  25903  dvply1  26211  vieta1lem2  26239  aaliou3lem4  26274  dvtaylp  26298  pserdvlem2  26358  advlogexp  26584  log2ublem2  26877  log2ublem3  26878  log2ub  26879  ftalem5  27007  cht1  27095  1sgmprm  27130  lgsquadlem2  27312  axlowdimlem16  28928  finsumvtxdg2ssteplem4  29520  rusgrnumwwlks  29945  cos9thpiminplylem3  33787  signsvf0  34583  signsvf1  34584  repr0  34614  sumeq12si  36216  cbvsumvw2  36259  sumcubes  42325  k0004val0  44166  binomcxplemnotnn0  44368  fsumiunss  45594  dvnmul  45960  stoweidlem17  46034  dirkertrigeqlem1  46115  etransclem24  46275  etransclem35  46286