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

Metamath Proof Explorer

Theorem sumeq1i

Description: Equality inference for sum. (Contributed by NM, 2-Jan-2006)

Ref Expression
Hypothesis sumeq1i.1 ⊢ A = B
Assertion sumeq1i ⊢ ∑ k ∈ A C = ∑ k ∈ B C

Proof

Step Hyp Ref Expression
1 sumeq1i.1 ⊢ A = B
2 sumeq1 ⊢ A = B → ∑ k ∈ A C = ∑ k ∈ B C
3 1 2 ax-mp ⊢ ∑ k ∈ A C = ∑ k ∈ B C