Theorem sumeq1i 15718

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

Syntax hints:   = wceq 1540  Σcsu 15707

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 2708

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 2715  df-cleq 2728  df-clel 2810  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-opab 5187  df-mpt 5207  df-xp 5665  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6295  df-iota 6489  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-ov 7413  df-oprab 7414  df-mpo 7415  df-frecs 8285  df-wrecs 8316  df-recs 8390  df-rdg 8429  df-seq 14025  df-sum 15708

This theorem is referenced by:  sumeq12i  15720  fsump1i  15790  fsum2d  15792  fsumxp  15793  isumnn0nn  15863  arisum  15881  arisum2  15882  geo2sum  15894  bpoly0  16071  bpoly1  16072  bpoly2  16078  bpoly3  16079  bpoly4  16080  efsep  16133  ef4p  16136  rpnnen2lem12  16248  ovolicc2lem4  25478  itg10  25646  dveflem  25940  dvply1  26248  vieta1lem2  26276  aaliou3lem4  26311  dvtaylp  26335  pserdvlem2  26395  advlogexp  26621  log2ublem2  26914  log2ublem3  26915  log2ub  26916  ftalem5  27044  cht1  27132  1sgmprm  27167  lgsquadlem2  27349  axlowdimlem16  28941  finsumvtxdg2ssteplem4  29533  rusgrnumwwlks  29961  cos9thpiminplylem3  33823  signsvf0  34617  signsvf1  34618  repr0  34648  sumeq12si  36226  cbvsumvw2  36269  sumcubes  42329  k0004val0  44145  binomcxplemnotnn0  44347  fsumiunss  45571  dvnmul  45939  stoweidlem17  46013  dirkertrigeqlem1  46094  etransclem24  46254  etransclem35  46265