Theorem nfsetrecs

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

	Ref	Expression
Hypothesis	nfsetrecs.1	⊢ Ⅎ 𝑥 𝐹
Assertion	nfsetrecs	⊢ Ⅎ 𝑥 setrecs ( 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		nfsetrecs.1	⊢ Ⅎ 𝑥 𝐹
2		df-setrecs	⊢ setrecs ( 𝐹 ) = ∪ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) }
3		nfv	⊢ Ⅎ 𝑥 𝑤 ⊆ 𝑦
4		nfv	⊢ Ⅎ 𝑥 𝑤 ⊆ 𝑧
5		nfcv	⊢ Ⅎ 𝑥 𝑤
6	1 5	nffv	⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑤 )
7		nfcv	⊢ Ⅎ 𝑥 𝑧
8	6 7	nfss	⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧
9	4 8	nfim	⊢ Ⅎ 𝑥 ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 )
10	3 9	nfim	⊢ Ⅎ 𝑥 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) )
11	10	nfal	⊢ Ⅎ 𝑥 ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) )
12		nfv	⊢ Ⅎ 𝑥 𝑦 ⊆ 𝑧
13	11 12	nfim	⊢ Ⅎ 𝑥 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 )
14	13	nfal	⊢ Ⅎ 𝑥 ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 )
15	14	nfab	⊢ Ⅎ 𝑥 { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) }
16	15	nfuni	⊢ Ⅎ 𝑥 ∪ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) }
17	2 16	nfcxfr	⊢ Ⅎ 𝑥 setrecs ( 𝐹 )