Theorem nfab 2304

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

Syntax hints:   F/wnf 1440   {cab 2143   F/_wnfc 2286

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515

This theorem depends on definitions:  df-bi 116  df-nf 1441  df-sb 1743  df-clab 2144  df-nfc 2288

This theorem is referenced by:  nfaba1  2305  nfrabxy  2637  sbcel12g  3046  sbceqg  3047  nfun  3264  nfpw  3557  nfpr  3611  nfop  3759  nfuni  3780  nfint  3819  intab  3838  nfiunxy  3877  nfiinxy  3878  nfiunya  3879  nfiinya  3880  nfiu1  3881  nfii1  3882  nfopab  4034  nfopab1  4035  nfopab2  4036  repizf2  4125  nfdm  4832  fun11iun  5437  eusvobj2  5812  nfoprab1  5872  nfoprab2  5873  nfoprab3  5874  nfoprab  5875  nfrecs  6256  nffrec  6345  nfixpxy  6664  nfixp1  6665