Theorem sumeq1i 15632

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

Syntax hints:   = wceq 1542  Σcsu 15621

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-xp 5638  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6267  df-iota 6456  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-ov 7371  df-oprab 7372  df-mpo 7373  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-rdg 8351  df-seq 13937  df-sum 15622

This theorem is referenced by:  sumeq12i  15634  fsump1i  15704  fsum2d  15706  fsumxp  15707  isumnn0nn  15777  arisum  15795  arisum2  15796  geo2sum  15808  bpoly0  15985  bpoly1  15986  bpoly2  15992  bpoly3  15993  bpoly4  15994  efsep  16047  ef4p  16050  rpnnen2lem12  16162  ovolicc2lem4  25489  itg10  25657  dveflem  25951  dvply1  26259  vieta1lem2  26287  aaliou3lem4  26322  dvtaylp  26346  pserdvlem2  26406  advlogexp  26632  log2ublem2  26925  log2ublem3  26926  log2ub  26927  ftalem5  27055  cht1  27143  1sgmprm  27178  lgsquadlem2  27360  axlowdimlem16  29042  finsumvtxdg2ssteplem4  29634  rusgrnumwwlks  30062  cos9thpiminplylem3  33962  signsvf0  34758  signsvf1  34759  repr0  34789  sumeq12si  36419  cbvsumvw2  36462  sumcubes  42683  k0004val0  44510  binomcxplemnotnn0  44712  fsumiunss  45935  dvnmul  46301  stoweidlem17  46375  dirkertrigeqlem1  46456  etransclem24  46616  etransclem35  46627