Theorem sumeq1i 15670

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

Syntax hints:   = wceq 1540  Σcsu 15659

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-xp 5647  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-pred 6277  df-iota 6467  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-ov 7393  df-oprab 7394  df-mpo 7395  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-rdg 8381  df-seq 13974  df-sum 15660

This theorem is referenced by:  sumeq12i  15672  fsump1i  15742  fsum2d  15744  fsumxp  15745  isumnn0nn  15815  arisum  15833  arisum2  15834  geo2sum  15846  bpoly0  16023  bpoly1  16024  bpoly2  16030  bpoly3  16031  bpoly4  16032  efsep  16085  ef4p  16088  rpnnen2lem12  16200  ovolicc2lem4  25428  itg10  25596  dveflem  25890  dvply1  26198  vieta1lem2  26226  aaliou3lem4  26261  dvtaylp  26285  pserdvlem2  26345  advlogexp  26571  log2ublem2  26864  log2ublem3  26865  log2ub  26866  ftalem5  26994  cht1  27082  1sgmprm  27117  lgsquadlem2  27299  axlowdimlem16  28891  finsumvtxdg2ssteplem4  29483  rusgrnumwwlks  29911  cos9thpiminplylem3  33781  signsvf0  34578  signsvf1  34579  repr0  34609  sumeq12si  36198  cbvsumvw2  36241  sumcubes  42308  k0004val0  44150  binomcxplemnotnn0  44352  fsumiunss  45580  dvnmul  45948  stoweidlem17  46022  dirkertrigeqlem1  46103  etransclem24  46263  etransclem35  46274