Theorem sumeq1i 15730

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

Syntax hints:   = wceq 1537  Σcsu 15719

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-mpt 5232  df-xp 5695  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-iota 6516  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-ov 7434  df-oprab 7435  df-mpo 7436  df-frecs 8305  df-wrecs 8336  df-recs 8410  df-rdg 8449  df-seq 14040  df-sum 15720

This theorem is referenced by:  sumeq12i  15732  fsump1i  15802  fsum2d  15804  fsumxp  15805  isumnn0nn  15875  arisum  15893  arisum2  15894  geo2sum  15906  bpoly0  16083  bpoly1  16084  bpoly2  16090  bpoly3  16091  bpoly4  16092  efsep  16143  ef4p  16146  rpnnen2lem12  16258  ovolicc2lem4  25569  itg10  25737  dveflem  26032  dvply1  26340  vieta1lem2  26368  aaliou3lem4  26403  dvtaylp  26427  pserdvlem2  26487  advlogexp  26712  log2ublem2  27005  log2ublem3  27006  log2ub  27007  ftalem5  27135  cht1  27223  1sgmprm  27258  lgsquadlem2  27440  axlowdimlem16  28987  finsumvtxdg2ssteplem4  29581  rusgrnumwwlks  30004  signsvf0  34574  signsvf1  34575  repr0  34605  sumeq12si  36185  cbvsumvw2  36229  sumcubes  42326  k0004val0  44144  binomcxplemnotnn0  44352  fsumiunss  45531  dvnmul  45899  stoweidlem17  45973  dirkertrigeqlem1  46054  etransclem24  46214  etransclem35  46225