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

Metamath Proof Explorer

Theorem sumsn

Description: A sum of a singleton is the term. (Contributed by Mario Carneiro, 22-Apr-2014)

Ref Expression
Hypothesis fsum1.1 ⊢ k = M → A = B
Assertion sumsn ⊢ M ∈ V ∧ B ∈ ℂ → ∑ k ∈ M A = B

Proof

Step Hyp Ref Expression
1 fsum1.1 ⊢ k = M → A = B
2 nfcv ⊢ Ⅎ _ k B
3 2 1 sumsnf ⊢ M ∈ V ∧ B ∈ ℂ → ∑ k ∈ M A = B