Metamath Proof Explorer


Theorem sumeq2i

Description: Equality inference for sum. (Contributed by NM, 3-Dec-2005)

Ref Expression
Hypothesis sumeq2i.1 ( 𝑘𝐴𝐵 = 𝐶 )
Assertion sumeq2i Σ 𝑘𝐴 𝐵 = Σ 𝑘𝐴 𝐶

Proof

Step Hyp Ref Expression
1 sumeq2i.1 ( 𝑘𝐴𝐵 = 𝐶 )
2 sumeq2 ( ∀ 𝑘𝐴 𝐵 = 𝐶 → Σ 𝑘𝐴 𝐵 = Σ 𝑘𝐴 𝐶 )
3 2 1 mprg Σ 𝑘𝐴 𝐵 = Σ 𝑘𝐴 𝐶