Theorem sumeq1i 15747

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

Syntax hints:   = wceq 1567  Σcsu 15736

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-opab 5178  df-mpt 5197  df-xp 5668  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-pred 6303  df-iota 6493  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7414  df-oprab 7415  df-mpo 7416  df-frecs 8277  df-wrecs 8308  df-recs 8357  df-rdg 8396  df-seq 14037  df-sum 15737

This theorem is referenced by:  sumeq12i  15749  fsump1i  15819  fsum2d  15821  fsumxp  15822  isumnn0nn  15895  arisum  15913  arisum2  15914  geo2sum  15926  bpoly0  16103  bpoly1  16104  bpoly2  16110  bpoly3  16111  bpoly4  16112  efsep  16165  ef4p  16168  rpnnen2lem12  16280  ovolicc2lem4  25647  itg10  25815  dveflem  26106  dvply1  26413  vieta1lem2  26440  aaliou3lem4  26475  dvtaylp  26498  pserdvlem2  26556  advlogexp  26785  log2ublem2  27077  log2ublem3  27078  log2ub  27079  ftalem5  27206  cht1  27294  1sgmprm  27328  lgsquadlem2  27510  axlowdimlem16  29247  finsumvtxdg2ssteplem4  29838  rusgrnumwwlks  30266  cos9thpiminplylem3  34118  signsvf0  34911  signsvf1  34912  repr0  34942  sumeq12si  36603  cbvsumvw2  36646  sumcubes  42963  k0004val0  44771  binomcxplemnotnn0  44957  fsumiunss  46182  dvnmul  46548  stoweidlem17  46622  dirkertrigeqlem1  46703  etransclem24  46863  etransclem35  46874