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 e. V /\ B e. CC ) -> sum_ k e. { M } A = B )

Proof

Step Hyp Ref Expression
1 fsum1.1 
 |-  ( k = M -> A = B )
2 nfcv 
 |-  F/_ k B
3 2 1 sumsnf 
 |-  ( ( M e. V /\ B e. CC ) -> sum_ k e. { M } A = B )