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	⊢ 𝐵 = setrecs ( 𝐹 )
	setrec2.c	⊢ ( 𝜑 → ∀ 𝑎 ( 𝑎 ⊆ 𝐶 → ( 𝐹 ‘ 𝑎 ) ⊆ 𝐶 ) )
Assertion	setrec2v	⊢ ( 𝜑 → 𝐵 ⊆ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		setrec2.b	⊢ 𝐵 = setrecs ( 𝐹 )
2		setrec2.c	⊢ ( 𝜑 → ∀ 𝑎 ( 𝑎 ⊆ 𝐶 → ( 𝐹 ‘ 𝑎 ) ⊆ 𝐶 ) )
3		nfcv	⊢ Ⅎ 𝑎 𝐹
4	3 1 2	setrec2	⊢ ( 𝜑 → 𝐵 ⊆ 𝐶 )