Theorem nfab 2377

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

Syntax hints:   F/wnf 1506   {cab 2215   F/_wnfc 2359

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-nfc 2361

This theorem is referenced by:  nfaba1  2378  nfrabw  2712  sbcel12g  3139  sbceqg  3140  nfun  3360  nfpw  3662  nfpr  3716  nfop  3873  nfuni  3894  nfint  3933  intab  3952  nfiunxy  3991  nfiinxy  3992  nfiunya  3993  nfiinya  3994  nfiu1  3995  nfii1  3996  nfopab  4152  nfopab1  4153  nfopab2  4154  repizf2  4246  nfdm  4968  fun11iun  5593  eusvobj2  5987  nfoprab1  6053  nfoprab2  6054  nfoprab3  6055  nfoprab  6056  nfrecs  6453  nffrec  6542  nfixpxy  6864  nfixp1  6865  nfwrd  11100