Metamath Proof Explorer


Theorem sumeq2

Description: Equality theorem for sum. (Contributed by NM, 11-Dec-2005) (Revised by Mario Carneiro, 13-Jul-2013)

Ref Expression
Assertion sumeq2 ( ∀ 𝑘𝐴 𝐵 = 𝐶 → Σ 𝑘𝐴 𝐵 = Σ 𝑘𝐴 𝐶 )

Proof

Step Hyp Ref Expression
1 fveq2 ( 𝐵 = 𝐶 → ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) )
2 1 ralimi ( ∀ 𝑘𝐴 𝐵 = 𝐶 → ∀ 𝑘𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) )
3 sumeq2ii ( ∀ 𝑘𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) → Σ 𝑘𝐴 𝐵 = Σ 𝑘𝐴 𝐶 )
4 2 3 syl ( ∀ 𝑘𝐴 𝐵 = 𝐶 → Σ 𝑘𝐴 𝐵 = Σ 𝑘𝐴 𝐶 )