Metamath Proof Explorer

Theorem nfsetrecs

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

Ref Expression
Hypothesis nfsetrecs.1 
|- F/_ x F
Assertion nfsetrecs 
|- F/_ x setrecs ( F )

Proof

Step Hyp Ref Expression
1 nfsetrecs.1 
 |-  F/_ x F
2 df-setrecs 
 |-  setrecs ( F ) = U. { y | A. z ( A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) -> y C_ z ) }
3 nfv 
 |-  F/ x w C_ y
4 nfv 
 |-  F/ x w C_ z
5 nfcv 
 |-  F/_ x w
6 1 5 nffv 
 |-  F/_ x ( F ` w )
7 nfcv 
 |-  F/_ x z
8 6 7 nfss 
 |-  F/ x ( F ` w ) C_ z
9 4 8 nfim 
 |-  F/ x ( w C_ z -> ( F ` w ) C_ z )
10 3 9 nfim 
 |-  F/ x ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) )
11 10 nfal 
 |-  F/ x A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) )
12 nfv 
 |-  F/ x y C_ z
13 11 12 nfim 
 |-  F/ x ( A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) -> y C_ z )
14 13 nfal 
 |-  F/ x A. z ( A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) -> y C_ z )
15 14 nfab 
 |-  F/_ x { y | A. z ( A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) -> y C_ z ) }
16 15 nfuni 
 |-  F/_ x U. { y | A. z ( A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) -> y C_ z ) }
17 2 16 nfcxfr 
 |-  F/_ x setrecs ( F )