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	⊢ ( ( 𝜑 ∧ 𝑘 = 𝑀 ) → 𝐴 = 𝐵 )
	esumsn.2	⊢ ( 𝜑 → 𝑀 ∈ 𝑉 )
	esumsn.3	⊢ ( 𝜑 → 𝐵 ∈ ( 0 [,] +∞ ) )
Assertion	esumsn	⊢ ( 𝜑 → Σ* 𝑘 ∈ { 𝑀 } 𝐴 = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		esumsn.1	⊢ ( ( 𝜑 ∧ 𝑘 = 𝑀 ) → 𝐴 = 𝐵 )
2		esumsn.2	⊢ ( 𝜑 → 𝑀 ∈ 𝑉 )
3		esumsn.3	⊢ ( 𝜑 → 𝐵 ∈ ( 0 [,] +∞ ) )
4		nfcv	⊢ Ⅎ 𝑘 𝐵
5	4 1 2 3	esumsnf	⊢ ( 𝜑 → Σ* 𝑘 ∈ { 𝑀 } 𝐴 = 𝐵 )