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  3140  sbceqg  3141  nfun  3361  nfpw  3663  nfpr  3717  nfop  3876  nfuni  3897  nfint  3936  intab  3955  nfiunxy  3994  nfiinxy  3995  nfiunya  3996  nfiinya  3997  nfiu1  3998  nfii1  3999  nfopab  4155  nfopab1  4156  nfopab2  4157  repizf2  4250  nfdm  4974  fun11iun  5601  eusvobj2  5999  nfoprab1  6065  nfoprab2  6066  nfoprab3  6067  nfoprab  6068  nfrecs  6468  nffrec  6557  nfixpxy  6881  nfixp1  6882  nfwrd  11132