Theorem nfab 2336

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

Syntax hints:   F/wnf 1470   {cab 2174   F/_wnfc 2318

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 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545

This theorem depends on definitions:  df-bi 117  df-nf 1471  df-sb 1773  df-clab 2175  df-nfc 2320

This theorem is referenced by:  nfaba1  2337  nfrabxy  2670  sbcel12g  3086  sbceqg  3087  nfun  3305  nfpw  3602  nfpr  3656  nfop  3808  nfuni  3829  nfint  3868  intab  3887  nfiunxy  3926  nfiinxy  3927  nfiunya  3928  nfiinya  3929  nfiu1  3930  nfii1  3931  nfopab  4085  nfopab1  4086  nfopab2  4087  repizf2  4176  nfdm  4885  fun11iun  5496  eusvobj2  5876  nfoprab1  5939  nfoprab2  5940  nfoprab3  5941  nfoprab  5942  nfrecs  6325  nffrec  6414  nfixpxy  6734  nfixp1  6735