Theorem nfesum2

Description: Bound-variable hypothesis builder for extended sum. (Contributed by Thierry Arnoux, 2-May-2020)

	Ref	Expression
Hypotheses	nfesum2.1	⊢ Ⅎ 𝑥 𝐴
	nfesum2.2	⊢ Ⅎ 𝑥 𝐵
Assertion	nfesum2	⊢ Ⅎ 𝑥 Σ* 𝑘 ∈ 𝐴 𝐵

Proof

Step	Hyp	Ref	Expression
1		nfesum2.1	⊢ Ⅎ 𝑥 𝐴
2		nfesum2.2	⊢ Ⅎ 𝑥 𝐵
3		df-esum	⊢ Σ* 𝑘 ∈ 𝐴 𝐵 = ∪ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) )
4		nfcv	⊢ Ⅎ 𝑥 ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) )
5		nfcv	⊢ Ⅎ 𝑥 tsums
6	1 2	nfmpt	⊢ Ⅎ 𝑥 ( 𝑘 ∈ 𝐴 ↦ 𝐵 )
7	4 5 6	nfov	⊢ Ⅎ 𝑥 ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) )
8	7	nfuni	⊢ Ⅎ 𝑥 ∪ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) )
9	3 8	nfcxfr	⊢ Ⅎ 𝑥 Σ* 𝑘 ∈ 𝐴 𝐵