Theorem nfab 2223

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

Syntax hints:   F/wnf 1389   {cab 2067   F/_wnfc 2206

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 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468

This theorem depends on definitions:  df-bi 115  df-nf 1390  df-sb 1686  df-clab 2068  df-nfc 2208

This theorem is referenced by:  nfaba1  2224  nfrabxy  2534  sbcel12g  2921  sbceqg  2922  nfun  3128  nfpw  3394  nfpr  3442  nfop  3586  nfuni  3607  nfint  3646  intab  3665  nfiunxy  3704  nfiinxy  3705  nfiunya  3706  nfiinya  3707  nfiu1  3708  nfii1  3709  nfopab  3846  nfopab1  3847  nfopab2  3848  repizf2  3936  nfdm  4596  fun11iun  5167  eusvobj2  5518  nfoprab1  5574  nfoprab2  5575  nfoprab3  5576  nfoprab  5577  nfrecs  5945  nffrec  6005