Theorem nfab 2391

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

Syntax hints:   F/wnf 1509   {cab 2220   F/_wnfc 2373

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-nfc 2375

This theorem is referenced by:  nfaba1  2392  nfrabw  2727  sbcel12g  3156  sbceqg  3157  nfun  3379  nfpw  3690  nfpr  3744  nfop  3904  nfuni  3925  nfint  3964  intab  3983  nfiunxy  4022  nfiinxy  4023  nfiunya  4024  nfiinya  4025  nfiu1  4026  nfii1  4027  nfopab  4183  nfopab1  4184  nfopab2  4185  repizf2  4280  nfdm  5006  fun11iun  5640  eusvobj2  6044  nfoprab1  6110  nfoprab2  6111  nfoprab3  6112  nfoprab  6113  nfrecs  6551  nffrec  6640  nfixpxy  6965  nfixp1  6966  nfwrd  11278