Theorem sumeq1i 15653

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

Syntax hints:   = wceq 1542  Σcsu 15642

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-xp 5631  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6260  df-iota 6449  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-ov 7364  df-oprab 7365  df-mpo 7366  df-frecs 8225  df-wrecs 8256  df-recs 8305  df-rdg 8343  df-seq 13958  df-sum 15643

This theorem is referenced by:  sumeq12i  15655  fsump1i  15725  fsum2d  15727  fsumxp  15728  isumnn0nn  15801  arisum  15819  arisum2  15820  geo2sum  15832  bpoly0  16009  bpoly1  16010  bpoly2  16016  bpoly3  16017  bpoly4  16018  efsep  16071  ef4p  16074  rpnnen2lem12  16186  ovolicc2lem4  25500  itg10  25668  dveflem  25959  dvply1  26263  vieta1lem2  26291  aaliou3lem4  26326  dvtaylp  26350  pserdvlem2  26409  advlogexp  26635  log2ublem2  26927  log2ublem3  26928  log2ub  26929  ftalem5  27057  cht1  27145  1sgmprm  27179  lgsquadlem2  27361  axlowdimlem16  29043  finsumvtxdg2ssteplem4  29635  rusgrnumwwlks  30063  cos9thpiminplylem3  33947  signsvf0  34743  signsvf1  34744  repr0  34774  sumeq12si  36404  cbvsumvw2  36447  sumcubes  42762  k0004val0  44602  binomcxplemnotnn0  44804  fsumiunss  46026  dvnmul  46392  stoweidlem17  46466  dirkertrigeqlem1  46547  etransclem24  46707  etransclem35  46718