Theorem nfab 2391

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

Syntax hints:   F/wnf 1509   {cab 2220   F/_wnfc 2373

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-nfc 2375

This theorem is referenced by:  nfaba1  2392  nfrabw  2727  sbcel12g  3155  sbceqg  3156  nfun  3377  nfpw  3687  nfpr  3741  nfop  3901  nfuni  3922  nfint  3961  intab  3980  nfiunxy  4019  nfiinxy  4020  nfiunya  4021  nfiinya  4022  nfiu1  4023  nfii1  4024  nfopab  4180  nfopab1  4181  nfopab2  4182  repizf2  4277  nfdm  5003  fun11iun  5637  eusvobj2  6038  nfoprab1  6104  nfoprab2  6105  nfoprab3  6106  nfoprab  6107  nfrecs  6540  nffrec  6629  nfixpxy  6954  nfixp1  6955  nfwrd  11257