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 ⊢ 𝐴 = 𝐵
sumeq12i.2 ⊢ ( 𝑘 ∈ 𝐴 → 𝐶 = 𝐷 )
Assertion sumeq12i Σ 𝑘 ∈ 𝐴 𝐶 = Σ 𝑘 ∈ 𝐵 𝐷

Proof

Step Hyp Ref Expression
1 sumeq12i.1 ⊢ 𝐴 = 𝐵
2 sumeq12i.2 ⊢ ( 𝑘 ∈ 𝐴 → 𝐶 = 𝐷 )
3 2 sumeq2i ⊢ Σ 𝑘 ∈ 𝐴 𝐶 = Σ 𝑘 ∈ 𝐴 𝐷
4 1 sumeq1i ⊢ Σ 𝑘 ∈ 𝐴 𝐷 = Σ 𝑘 ∈ 𝐵 𝐷
5 3 4 eqtri ⊢ Σ 𝑘 ∈ 𝐴 𝐶 = Σ 𝑘 ∈ 𝐵 𝐷