This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ∀ k ∈ A B = C → ∑ k ∈ A B = ∑ k ∈ A C

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ B = C → I ⁡ B = I ⁡ C
2 1 ralimi ⊢ ∀ k ∈ A B = C → ∀ k ∈ A I ⁡ B = I ⁡ C
3 sumeq2ii ⊢ ∀ k ∈ A I ⁡ B = I ⁡ C → ∑ k ∈ A B = ∑ k ∈ A C
4 2 3 syl ⊢ ∀ k ∈ A B = C → ∑ k ∈ A B = ∑ k ∈ A C