Theorem nfsetrecs

Description: Bound-variable hypothesis builder for setrecs . (Contributed by Emmett Weisz, 21-Oct-2021)

	Ref	Expression
Hypothesis	nfsetrecs.1	$$⊢\underset{\_}{Ⅎ}xF$$
Assertion	nfsetrecs	$$⊢\underset{\_}{Ⅎ}x\mathrm{setrecs}\left(F\right)$$

Proof

Step	Hyp	Ref	Expression
1		nfsetrecs.1	$$⊢\underset{\_}{Ⅎ}xF$$
2		df-setrecs	$$⊢\mathrm{setrecs}\left(F\right)=\bigcup \left\{y|\forall z\left(\forall w\left(w\subseteq y\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to y\subseteq z\right)\right\}$$
3		nfv	$$⊢Ⅎxw\subseteq y$$
4		nfv	$$⊢Ⅎxw\subseteq z$$
5		nfcv	$$⊢\underset{\_}{Ⅎ}xw$$
6	1 5	nffv	$$⊢\underset{\_}{Ⅎ}xF\left(w\right)$$
7		nfcv	$$⊢\underset{\_}{Ⅎ}xz$$
8	6 7	nfss	$$⊢ℲxF\left(w\right)\subseteq z$$
9	4 8	nfim	$$⊢Ⅎx\left(w\subseteq z\to F\left(w\right)\subseteq z\right)$$
10	3 9	nfim	$$⊢Ⅎx\left(w\subseteq y\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)$$
11	10	nfal	$$⊢Ⅎx\forall w\left(w\subseteq y\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)$$
12		nfv	$$⊢Ⅎxy\subseteq z$$
13	11 12	nfim	$$⊢Ⅎx\left(\forall w\left(w\subseteq y\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to y\subseteq z\right)$$
14	13	nfal	$$⊢Ⅎx\forall z\left(\forall w\left(w\subseteq y\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to y\subseteq z\right)$$
15	14	nfab	$$⊢\underset{\_}{Ⅎ}x\left\{y|\forall z\left(\forall w\left(w\subseteq y\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to y\subseteq z\right)\right\}$$
16	15	nfuni	$$⊢\underset{\_}{Ⅎ}x\bigcup \left\{y|\forall z\left(\forall w\left(w\subseteq y\to \left(w\subseteq z\to F\left(w\right)\subseteq z\right)\right)\to y\subseteq z\right)\right\}$$
17	2 16	nfcxfr	$$⊢\underset{\_}{Ⅎ}x\mathrm{setrecs}\left(F\right)$$