Theorem sumeq1i 15663

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

Syntax hints:   = wceq 1540  Σcsu 15652

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-xp 5644  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-iota 6464  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-ov 7390  df-oprab 7391  df-mpo 7392  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-seq 13967  df-sum 15653

This theorem is referenced by:  sumeq12i  15665  fsump1i  15735  fsum2d  15737  fsumxp  15738  isumnn0nn  15808  arisum  15826  arisum2  15827  geo2sum  15839  bpoly0  16016  bpoly1  16017  bpoly2  16023  bpoly3  16024  bpoly4  16025  efsep  16078  ef4p  16081  rpnnen2lem12  16193  ovolicc2lem4  25421  itg10  25589  dveflem  25883  dvply1  26191  vieta1lem2  26219  aaliou3lem4  26254  dvtaylp  26278  pserdvlem2  26338  advlogexp  26564  log2ublem2  26857  log2ublem3  26858  log2ub  26859  ftalem5  26987  cht1  27075  1sgmprm  27110  lgsquadlem2  27292  axlowdimlem16  28884  finsumvtxdg2ssteplem4  29476  rusgrnumwwlks  29904  cos9thpiminplylem3  33774  signsvf0  34571  signsvf1  34572  repr0  34602  sumeq12si  36191  cbvsumvw2  36234  sumcubes  42301  k0004val0  44143  binomcxplemnotnn0  44345  fsumiunss  45573  dvnmul  45941  stoweidlem17  46015  dirkertrigeqlem1  46096  etransclem24  46256  etransclem35  46267