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

Metamath Proof Explorer

Theorem sumeq2sdvOLD

Description: Obsolete version of sumeq2sdv as of 14-Aug-2025. (Contributed by NM, 3-Jan-2006) (Proof shortened by Glauco Siliprandi, 5-Apr-2020) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 sumeq2sdvOLD.1 ⊢ φ → B = C
2 1 ralrimivw ⊢ φ → ∀ k ∈ A B = C
3 2 sumeq2d ⊢ φ → ∑ k ∈ A B = ∑ k ∈ A C