Theorem sumsns

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

	Ref	Expression
Assertion	sumsns	|- ( ( M e. V /\ [_ M / k ]_ A e. CC ) -> sum_ k e. { M } A = [_ M / k ]_ A )

Proof

Step	Hyp	Ref	Expression
1		nfcv	|- F/_ n A
2		nfcsb1v	|- F/_ k [_ n / k ]_ A
3		csbeq1a	|- ( k = n -> A = [_ n / k ]_ A )
4	1 2 3	cbvsumi	|- sum_ k e. { M } A = sum_ n e. { M } [_ n / k ]_ A
5		csbeq1	|- ( n = M -> [_ n / k ]_ A = [_ M / k ]_ A )
6	5	sumsn	|- ( ( M e. V /\ [_ M / k ]_ A e. CC ) -> sum_ n e. { M } [_ n / k ]_ A = [_ M / k ]_ A )
7	4 6	eqtrid	|- ( ( M e. V /\ [_ M / k ]_ A e. CC ) -> sum_ k e. { M } A = [_ M / k ]_ A )