Theorem nfab 2355

Description: Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.)

Hypothesis

Ref	Expression
nfab.1	|- F/ x ph

Assertion

Ref	Expression
nfab	|- F/_ x { y | ph }

Proof of Theorem nfab

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfab.1	. . 3 |- F/ x ph
2	1	nfsab 2199	. 2 |- F/ x z e. { y | ph }
3	2	nfci 2340	1 |- F/_ x { y | ph }

Syntax hints:   F/wnf 1484   {cab 2193   F/_wnfc 2337

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2194  df-nfc 2339

This theorem is referenced by:  nfaba1  2356  nfrabw  2689  sbcel12g  3116  sbceqg  3117  nfun  3337  nfpw  3639  nfpr  3693  nfop  3849  nfuni  3870  nfint  3909  intab  3928  nfiunxy  3967  nfiinxy  3968  nfiunya  3969  nfiinya  3970  nfiu1  3971  nfii1  3972  nfopab  4128  nfopab1  4129  nfopab2  4130  repizf2  4222  nfdm  4941  fun11iun  5565  eusvobj2  5953  nfoprab1  6017  nfoprab2  6018  nfoprab3  6019  nfoprab  6020  nfrecs  6416  nffrec  6505  nfixpxy  6827  nfixp1  6828  nfwrd  11059