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	$$⊢\left(\phi \wedge k=M\right)\to A=B$$
	esumsn.2	$$⊢\phi \to M\in V$$
	esumsn.3	$$⊢\phi \to B\in \left[0,\mathrm{+\infty }\right]$$
Assertion	esumsn	$$⊢\phi \to \underset{k\in \left\{M\right\}}{{\sum }^{*}}A=B$$

Proof

Step	Hyp	Ref	Expression
1		esumsn.1	$$⊢\left(\phi \wedge k=M\right)\to A=B$$
2		esumsn.2	$$⊢\phi \to M\in V$$
3		esumsn.3	$$⊢\phi \to B\in \left[0,\mathrm{+\infty }\right]$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}kB$$
5	4 1 2 3	esumsnf	$$⊢\phi \to \underset{k\in \left\{M\right\}}{{\sum }^{*}}A=B$$