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

Metamath Proof Explorer

Theorem sumeq12i

Description: Equality inference for sum. (Contributed by FL, 10-Dec-2006)

Ref Expression
Hypotheses sumeq12i.1 ⊢ A = B
sumeq12i.2 ⊢ k ∈ A → C = D
Assertion sumeq12i ⊢ ∑ k ∈ A C = ∑ k ∈ B D

Proof

Step Hyp Ref Expression
1 sumeq12i.1 ⊢ A = B
2 sumeq12i.2 ⊢ k ∈ A → C = D
3 2 sumeq2i ⊢ ∑ k ∈ A C = ∑ k ∈ A D
4 1 sumeq1i ⊢ ∑ k ∈ A D = ∑ k ∈ B D
5 3 4 eqtri ⊢ ∑ k ∈ A C = ∑ k ∈ B D