Metamath Proof Explorer

Theorem nfsetrecs

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

Ref Expression
Hypothesis nfsetrecs.1 ⊢ Ⅎ _ x F
Assertion nfsetrecs ⊢ Ⅎ _ x setrecs ⁡ F

Proof

Step Hyp Ref Expression
1 nfsetrecs.1 ⊢ Ⅎ _ x F
2 df-setrecs ⊢ setrecs ⁡ F = ⋃ y | ∀ z ∀ w w ⊆ y → w ⊆ z → F ⁡ w ⊆ z → y ⊆ z
3 nfv ⊢ Ⅎ x w ⊆ y
4 nfv ⊢ Ⅎ x w ⊆ z
5 nfcv ⊢ Ⅎ _ x w
6 1 5 nffv ⊢ Ⅎ _ x F ⁡ w
7 nfcv ⊢ Ⅎ _ x z
8 6 7 nfss ⊢ Ⅎ x F ⁡ w ⊆ z
9 4 8 nfim ⊢ Ⅎ x w ⊆ z → F ⁡ w ⊆ z
10 3 9 nfim ⊢ Ⅎ x w ⊆ y → w ⊆ z → F ⁡ w ⊆ z
11 10 nfal ⊢ Ⅎ x ∀ w w ⊆ y → w ⊆ z → F ⁡ w ⊆ z
12 nfv ⊢ Ⅎ x y ⊆ z
13 11 12 nfim ⊢ Ⅎ x ∀ w w ⊆ y → w ⊆ z → F ⁡ w ⊆ z → y ⊆ z
14 13 nfal ⊢ Ⅎ x ∀ z ∀ w w ⊆ y → w ⊆ z → F ⁡ w ⊆ z → y ⊆ z
15 14 nfab ⊢ Ⅎ _ x y | ∀ z ∀ w w ⊆ y → w ⊆ z → F ⁡ w ⊆ z → y ⊆ z
16 15 nfuni ⊢ Ⅎ _ x ⋃ y | ∀ z ∀ w w ⊆ y → w ⊆ z → F ⁡ w ⊆ z → y ⊆ z
17 2 16 nfcxfr ⊢ Ⅎ _ x setrecs ⁡ F