Theorem nfab 2324

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

Syntax hints:   F/wnf 1460   {cab 2163   F/_wnfc 2306

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-nfc 2308

This theorem is referenced by:  nfaba1  2325  nfrabxy  2657  sbcel12g  3072  sbceqg  3073  nfun  3291  nfpw  3588  nfpr  3642  nfop  3793  nfuni  3814  nfint  3853  intab  3872  nfiunxy  3911  nfiinxy  3912  nfiunya  3913  nfiinya  3914  nfiu1  3915  nfii1  3916  nfopab  4069  nfopab1  4070  nfopab2  4071  repizf2  4160  nfdm  4868  fun11iun  5479  eusvobj2  5856  nfoprab1  5919  nfoprab2  5920  nfoprab3  5921  nfoprab  5922  nfrecs  6303  nffrec  6392  nfixpxy  6712  nfixp1  6713