Theorem nfesum2

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

	Ref	Expression
Hypotheses	nfesum2.1	$$⊢\underset{\_}{Ⅎ}xA$$
	nfesum2.2	$$⊢\underset{\_}{Ⅎ}xB$$
Assertion	nfesum2	$$⊢\underset{\_}{Ⅎ}x\underset{k\in A}{{\sum }^{*}}B$$

Proof

Step	Hyp	Ref	Expression
1		nfesum2.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		nfesum2.2	$$⊢\underset{\_}{Ⅎ}xB$$
3		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)$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}x\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)$$
5		nfcv	$$⊢\underset{\_}{Ⅎ}x\mathrm{tsums}$$
6	1 2	nfmpt	$$⊢\underset{\_}{Ⅎ}x\left(k\in A⟼B\right)$$
7	4 5 6	nfov	$$⊢\underset{\_}{Ⅎ}x\left(\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)\mathrm{tsums}\left(k\in A⟼B\right)\right)$$
8	7	nfuni	$$⊢\underset{\_}{Ⅎ}x\bigcup \left(\left({ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left[0,\mathrm{+\infty }\right]\right)\mathrm{tsums}\left(k\in A⟼B\right)\right)$$
9	3 8	nfcxfr	$$⊢\underset{\_}{Ⅎ}x\underset{k\in A}{{\sum }^{*}}B$$