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