Theorem sumeq1i 15857

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

This proof depends on syntax axioms:   = wceq 1570  Σcsu 15846

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-xp 5657  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6303  df-iota 6493  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7421  df-oprab 7422  df-mpo 7423  df-frecs 8292  df-wrecs 8323  df-recs 8372  df-rdg 8411  df-seq 14138  df-sum 15847

This theorem is used by:  sumeq12i  15859  fsump1i  15928  fsum2d  15930  fsumxp  15931  isumnn0nn  16004  arisum  16022  arisum2  16023  geo2sum  16035  bpoly0  16209  bpoly1  16210  bpoly2  16216  bpoly3  16217  bpoly4  16218  efsep  16271  ef4p  16274  rpnnen2lem12  16386  ovolicc2lem4  25834  itg10  26002  dveflem  26292  dvply1  26598  vieta1lem2  26627  aaliou3lem4  26666  dvtaylp  26690  pserdvlem2  26748  advlogexp  26976  log2ublem2  27268  log2ublem3  27269  log2ub  27270  ftalem5  27397  cht1  27485  1sgmprm  27519  lgsquadlem2  27701  axlowdimlem16  29528  finsumvtxdg2ssteplem4  30122  rusgrnumwwlks  30559  cos9thpiminplylem3  34409  signsvf0  35202  signsvf1  35203  repr0  35233  sumeq12si  36972  cbvsumvw2  37015  sumcubes  43350  k0004val0  45139  binomcxplemnotnn0  45325  fsumiunss  46556  dvnmul  46922  stoweidlem17  46996  dirkertrigeqlem1  47077  etransclem24  47237  etransclem35  47248  crosspdotsumlem  50933