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

Metamath Proof Explorer

Theorem sumeq1d

Description: Equality deduction for sum. (Contributed by NM, 1-Nov-2005)

Ref Expression
Hypothesis sumeq1d.1 ⊢ φ → A = B
Assertion sumeq1d ⊢ φ → ∑ k ∈ A C = ∑ k ∈ B C

Proof

Step Hyp Ref Expression
1 sumeq1d.1 ⊢ φ → A = B
2 sumeq1 ⊢ A = B → ∑ k ∈ A C = ∑ k ∈ B C
3 1 2 syl ⊢ φ → ∑ k ∈ A C = ∑ k ∈ B C