Theorem nfcoll

Description: Bound-variable hypothesis builder for the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023)

	Ref	Expression
Hypotheses	nfcoll.1	$$⊢\underset{\_}{Ⅎ}xF$$
	nfcoll.2	$$⊢\underset{\_}{Ⅎ}xA$$
Assertion	nfcoll	$$⊢\underset{\_}{Ⅎ}x\left(FCollA\right)$$

Proof

Step	Hyp	Ref	Expression
1		nfcoll.1	$$⊢\underset{\_}{Ⅎ}xF$$
2		nfcoll.2	$$⊢\underset{\_}{Ⅎ}xA$$
3		df-coll	$$⊢\left(FCollA\right)=\bigcup _{y\in A}ScottF\left[\left\{y\right\}\right]$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}x\left\{y\right\}$$
5	1 4	nfima	$$⊢\underset{\_}{Ⅎ}xF\left[\left\{y\right\}\right]$$
6	5	nfscott	$$⊢\underset{\_}{Ⅎ}xScottF\left[\left\{y\right\}\right]$$
7	2 6	nfiun	$$⊢\underset{\_}{Ⅎ}x\bigcup _{y\in A}ScottF\left[\left\{y\right\}\right]$$
8	3 7	nfcxfr	$$⊢\underset{\_}{Ⅎ}x\left(FCollA\right)$$