Theorem setrec2v

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

	Ref	Expression
Hypotheses	setrec2.b	|- B = setrecs ( F )
	setrec2.c	|- ( ph -> A. a ( a C_ C -> ( F ` a ) C_ C ) )
Assertion	setrec2v	|- ( ph -> B C_ C )

Proof

Step	Hyp	Ref	Expression
1		setrec2.b	|- B = setrecs ( F )
2		setrec2.c	|- ( ph -> A. a ( a C_ C -> ( F ` a ) C_ C ) )
3		nfcv	|- F/_ a F
4	3 1 2	setrec2	|- ( ph -> B C_ C )