Theorem nfab 2224

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

Syntax hints:   F/wnf 1390   {cab 2068   F/_wnfc 2207

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469

This theorem depends on definitions:  df-bi 115  df-nf 1391  df-sb 1687  df-clab 2069  df-nfc 2209

This theorem is referenced by:  nfaba1  2225  nfrabxy  2535  sbcel12g  2922  sbceqg  2923  nfun  3129  nfpw  3402  nfpr  3450  nfop  3594  nfuni  3615  nfint  3654  intab  3673  nfiunxy  3712  nfiinxy  3713  nfiunya  3714  nfiinya  3715  nfiu1  3716  nfii1  3717  nfopab  3854  nfopab1  3855  nfopab2  3856  repizf2  3944  nfdm  4606  fun11iun  5178  eusvobj2  5529  nfoprab1  5585  nfoprab2  5586  nfoprab3  5587  nfoprab  5588  nfrecs  5956  nffrec  6045