Theorem nfab 2397

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

Syntax hints:   F/wnf 1513   {cab 2224   F/_wnfc 2379

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-nfc 2381

This theorem is referenced by:  nfaba1  2398  nfrabw  2733  sbcel12g  3162  sbceqg  3163  nfun  3385  nfpw  3704  nfpr  3758  nfop  3918  nfuni  3939  nfint  3978  intab  3997  nfiunxy  4036  nfiinxy  4037  nfiunya  4038  nfiinya  4039  nfiu1  4040  nfii1  4041  nfopab  4197  nfopab1  4198  nfopab2  4199  repizf2  4297  nfdm  5024  fun11iun  5658  eusvobj2  6064  nfoprab1  6130  nfoprab2  6131  nfoprab3  6132  nfoprab  6133  nfrecs  6571  nffrec  6660  nfixpxy  6992  nfixp1  6993  nfwrd  11314