Theorem nfab 2377

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 2221	. 2 ⊢ Ⅎ𝑥 𝑧 ∈ {𝑦 ∣ 𝜑}
3	2	nfci 2362	1 ⊢ Ⅎ𝑥{𝑦 ∣ 𝜑}

Syntax hints:  Ⅎwnf 1506  {cab 2215  Ⅎwnfc 2359

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-nfc 2361

This theorem is referenced by:  nfaba1  2378  nfrabw  2712  sbcel12g  3139  sbceqg  3140  nfun  3360  nfpw  3662  nfpr  3716  nfop  3873  nfuni  3894  nfint  3933  intab  3952  nfiunxy  3991  nfiinxy  3992  nfiunya  3993  nfiinya  3994  nfiu1  3995  nfii1  3996  nfopab  4152  nfopab1  4153  nfopab2  4154  repizf2  4247  nfdm  4971  fun11iun  5598  eusvobj2  5996  nfoprab1  6062  nfoprab2  6063  nfoprab3  6064  nfoprab  6065  nfrecs  6464  nffrec  6553  nfixpxy  6877  nfixp1  6878  nfwrd  11118