Theorem nfesum1

Description: Bound-variable hypothesis builder for extended sum. (Contributed by Thierry Arnoux, 19-Oct-2017)

	Ref	Expression
Hypothesis	nfesum1.1	$$⊢\underset{\_}{Ⅎ}kA$$
Assertion	nfesum1	$$⊢\underset{\_}{Ⅎ}k\underset{k\in A}{{\sum }^{*}}B$$

Proof

Step	Hyp	Ref	Expression
1		nfesum1.1	$$⊢\underset{\_}{Ⅎ}kA$$
2		df-esum	$$⊢\underset{k\in A}{{\sum }^{*}}B=\bigcup \left(\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)\mathrm{tsums}\left(k\in A⟼B\right)\right)$$
3		nfcv	$$⊢\underset{\_}{Ⅎ}k\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}k\mathrm{tsums}$$
5		nfmpt1	$$⊢\underset{\_}{Ⅎ}k\left(k\in A⟼B\right)$$
6	3 4 5	nfov	$$⊢\underset{\_}{Ⅎ}k\left(\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)\mathrm{tsums}\left(k\in A⟼B\right)\right)$$
7	6	nfuni	$$⊢\underset{\_}{Ⅎ}k\bigcup \left(\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)\mathrm{tsums}\left(k\in A⟼B\right)\right)$$
8	2 7	nfcxfr	$$⊢\underset{\_}{Ⅎ}k\underset{k\in A}{{\sum }^{*}}B$$