Theorem sumeq1i 15772

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

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

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 2148  ax-9 2156  ax-ext 2737

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 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-xp 5669  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6306  df-iota 6496  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7422  df-oprab 7423  df-mpo 7424  df-frecs 8284  df-wrecs 8315  df-recs 8364  df-rdg 8403  df-seq 14056  df-sum 15762

This theorem is used by:  sumeq12i  15774  fsump1i  15843  fsum2d  15845  fsumxp  15846  isumnn0nn  15919  arisum  15937  arisum2  15938  geo2sum  15950  bpoly0  16126  bpoly1  16127  bpoly2  16133  bpoly3  16134  bpoly4  16135  efsep  16188  ef4p  16191  rpnnen2lem12  16303  ovolicc2lem4  25730  itg10  25898  dveflem  26189  dvply1  26496  vieta1lem2  26523  aaliou3lem4  26560  dvtaylp  26584  pserdvlem2  26642  advlogexp  26871  log2ublem2  27163  log2ublem3  27164  log2ub  27165  ftalem5  27292  cht1  27380  1sgmprm  27414  lgsquadlem2  27596  axlowdimlem16  29362  finsumvtxdg2ssteplem4  29956  rusgrnumwwlks  30393  cos9thpiminplylem3  34238  signsvf0  35032  signsvf1  35033  repr0  35063  sumeq12si  36772  cbvsumvw2  36815  sumcubes  43132  k0004val0  44938  binomcxplemnotnn0  45124  fsumiunss  46349  dvnmul  46715  stoweidlem17  46789  dirkertrigeqlem1  46870  etransclem24  47030  etransclem35  47041  crosspdotsumlem  50703