Theorem nfab 2287

Description: Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.)

Hypothesis

Ref	Expression
nfab.1	⊢ Ⅎ𝑥𝜑

Assertion

Ref	Expression
nfab	⊢ Ⅎ𝑥{𝑦 ∣ 𝜑}

Proof of Theorem nfab

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfab.1	. . 3 ⊢ Ⅎ𝑥𝜑
2	1	nfsab 2132	. 2 ⊢ Ⅎ𝑥 𝑧 ∈ {𝑦 ∣ 𝜑}
3	2	nfci 2272	1 ⊢ Ⅎ𝑥{𝑦 ∣ 𝜑}

Syntax hints:  Ⅎwnf 1437  {cab 2126  Ⅎwnfc 2269

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-sb 1737  df-clab 2127  df-nfc 2271

This theorem is referenced by:  nfaba1  2288  nfrabxy  2614  sbcel12g  3022  sbceqg  3023  nfun  3237  nfpw  3528  nfpr  3581  nfop  3729  nfuni  3750  nfint  3789  intab  3808  nfiunxy  3847  nfiinxy  3848  nfiunya  3849  nfiinya  3850  nfiu1  3851  nfii1  3852  nfopab  4004  nfopab1  4005  nfopab2  4006  repizf2  4094  nfdm  4791  fun11iun  5396  eusvobj2  5768  nfoprab1  5828  nfoprab2  5829  nfoprab3  5830  nfoprab  5831  nfrecs  6212  nffrec  6301  nfixpxy  6619  nfixp1  6620