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\to A=B$$
Assertion	sumsn	$$⊢\left(M\in V\wedge B\in ℂ\right)\to \sum _{k\in \left\{M\right\}}A=B$$

Proof

Step	Hyp	Ref	Expression
1		fsum1.1	$$⊢k=M\to A=B$$
2		nfcv	$$⊢\underset{\_}{Ⅎ}kB$$
3	2 1	sumsnf	$$⊢\left(M\in V\wedge B\in ℂ\right)\to \sum _{k\in \left\{M\right\}}A=B$$