Theorem sumeq1i 14905

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

Syntax hints:   = wceq 1507  Σcsu 14893

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-ext 2745

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-clab 2754  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ral 3087  df-rex 3088  df-rab 3091  df-v 3411  df-dif 3828  df-un 3830  df-in 3832  df-ss 3839  df-nul 4174  df-if 4345  df-sn 4436  df-pr 4438  df-op 4442  df-uni 4707  df-br 4924  df-opab 4986  df-mpt 5003  df-xp 5406  df-cnv 5408  df-dm 5410  df-rn 5411  df-res 5412  df-ima 5413  df-pred 5980  df-iota 6146  df-f 6186  df-f1 6187  df-fo 6188  df-f1o 6189  df-fv 6190  df-ov 6973  df-oprab 6974  df-mpo 6975  df-wrecs 7743  df-recs 7805  df-rdg 7843  df-seq 13178  df-sum 14894

This theorem is referenced by:  sumeq12i  14907  fsump1i  14974  fsum2d  14976  fsumxp  14977  isumnn0nn  15047  arisum  15065  arisum2  15066  geo2sum  15079  bpoly0  15254  bpoly1  15255  bpoly2  15261  bpoly3  15262  bpoly4  15263  efsep  15313  ef4p  15316  rpnnen2lem12  15428  ovolicc2lem4  23814  itg10  23982  dveflem  24269  dvply1  24566  vieta1lem2  24593  aaliou3lem4  24628  dvtaylp  24651  pserdvlem2  24709  advlogexp  24929  log2ublem2  25217  log2ublem3  25218  log2ub  25219  ftalem5  25346  cht1  25434  1sgmprm  25467  lgsquadlem2  25649  axlowdimlem16  26436  finsumvtxdg2ssteplem4  27023  rusgrnumwwlks  27470  rusgrnumwwlksOLD  27471  signsvf0  31459  signsvf1  31460  repr0  31491  k0004val0  39812  binomcxplemnotnn0  40048  fsumiunss  41233  dvnmul  41604  stoweidlem17  41679  dirkertrigeqlem1  41760  etransclem24  41920  etransclem35  41931