Theorem sumeq1i 15644

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

Syntax hints:   = wceq 1542  Σcsu 15632

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-xp 5683  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-iota 6496  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-ov 7412  df-oprab 7413  df-mpo 7414  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-seq 13967  df-sum 15633

This theorem is referenced by:  sumeq12i  15646  fsump1i  15715  fsum2d  15717  fsumxp  15718  isumnn0nn  15788  arisum  15806  arisum2  15807  geo2sum  15819  bpoly0  15994  bpoly1  15995  bpoly2  16001  bpoly3  16002  bpoly4  16003  efsep  16053  ef4p  16056  rpnnen2lem12  16168  ovolicc2lem4  25037  itg10  25205  dveflem  25496  dvply1  25797  vieta1lem2  25824  aaliou3lem4  25859  dvtaylp  25882  pserdvlem2  25940  advlogexp  26163  log2ublem2  26452  log2ublem3  26453  log2ub  26454  ftalem5  26581  cht1  26669  1sgmprm  26702  lgsquadlem2  26884  axlowdimlem16  28215  finsumvtxdg2ssteplem4  28805  rusgrnumwwlks  29228  signsvf0  33591  signsvf1  33592  repr0  33623  sumcubes  41211  k0004val0  42905  binomcxplemnotnn0  43115  fsumiunss  44291  dvnmul  44659  stoweidlem17  44733  dirkertrigeqlem1  44814  etransclem24  44974  etransclem35  44985