Theorem esumsn

Description: The extended sum of a singleton is the term. (Contributed by Thierry Arnoux, 2-Jan-2017) (Shortened by Thierry Arnoux, 2-May-2020.)

	Ref	Expression
Hypotheses	esumsn.1	|- ( ( ph /\ k = M ) -> A = B )
	esumsn.2	|- ( ph -> M e. V )
	esumsn.3	|- ( ph -> B e. ( 0 [,] +oo ) )
Assertion	esumsn	|- ( ph -> sum* k e. { M } A = B )

Proof

Step	Hyp	Ref	Expression
1		esumsn.1	|- ( ( ph /\ k = M ) -> A = B )
2		esumsn.2	|- ( ph -> M e. V )
3		esumsn.3	|- ( ph -> B e. ( 0 [,] +oo ) )
4		nfcv	|- F/_ k B
5	4 1 2 3	esumsnf	|- ( ph -> sum* k e. { M } A = B )