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 ( 𝑘 = 𝑀𝐴 = 𝐵 )
Assertion sumsn ( ( 𝑀𝑉𝐵 ∈ ℂ ) → Σ 𝑘 ∈ { 𝑀 } 𝐴 = 𝐵 )

Proof

Step Hyp Ref Expression
1 fsum1.1 ( 𝑘 = 𝑀𝐴 = 𝐵 )
2 nfcv 𝑘 𝐵
3 2 1 sumsnf ( ( 𝑀𝑉𝐵 ∈ ℂ ) → Σ 𝑘 ∈ { 𝑀 } 𝐴 = 𝐵 )