Theorem nfab 2379

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 2223	. 2 |- F/ x z e. { y | ph }
3	2	nfci 2364	1 |- F/_ x { y | ph }

Syntax hints:   F/wnf 1508   {cab 2217   F/_wnfc 2361

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-nfc 2363

This theorem is referenced by:  nfaba1  2380  nfrabw  2714  sbcel12g  3142  sbceqg  3143  nfun  3363  nfpw  3665  nfpr  3719  nfop  3878  nfuni  3899  nfint  3938  intab  3957  nfiunxy  3996  nfiinxy  3997  nfiunya  3998  nfiinya  3999  nfiu1  4000  nfii1  4001  nfopab  4157  nfopab1  4158  nfopab2  4159  repizf2  4252  nfdm  4976  fun11iun  5605  eusvobj2  6007  nfoprab1  6073  nfoprab2  6074  nfoprab3  6075  nfoprab  6076  nfrecs  6476  nffrec  6565  nfixpxy  6889  nfixp1  6890  nfwrd  11149