Theorem setrec2v

Description: Version of setrec2 with a disjoint variable condition instead of a non-freeness hypothesis. (Contributed by Emmett Weisz, 6-Mar-2021)

	Ref	Expression
Hypotheses	setrec2.b	$$⊢B=\mathrm{setrecs}\left(F\right)$$
	setrec2.c	$$⊢\phi \to \forall a\left(a\subseteq C\to F\left(a\right)\subseteq C\right)$$
Assertion	setrec2v	$$⊢\phi \to B\subseteq C$$

Proof

Step	Hyp	Ref	Expression
1		setrec2.b	$$⊢B=\mathrm{setrecs}\left(F\right)$$
2		setrec2.c	$$⊢\phi \to \forall a\left(a\subseteq C\to F\left(a\right)\subseteq C\right)$$
3		nfcv	$$⊢\underset{\_}{Ⅎ}aF$$
4	3 1 2	setrec2	$$⊢\phi \to B\subseteq C$$