Theorem nfab 2357

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

Syntax hints:  Ⅎwnf 1486  {cab 2195  Ⅎwnfc 2339

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 713  ax-5 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-10 1531  ax-11 1532  ax-i12 1533  ax-bndl 1535  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561

This theorem depends on definitions:  df-bi 117  df-nf 1487  df-sb 1789  df-clab 2196  df-nfc 2341

This theorem is referenced by:  nfaba1  2358  nfrabw  2692  sbcel12g  3119  sbceqg  3120  nfun  3340  nfpw  3642  nfpr  3696  nfop  3852  nfuni  3873  nfint  3912  intab  3931  nfiunxy  3970  nfiinxy  3971  nfiunya  3972  nfiinya  3973  nfiu1  3974  nfii1  3975  nfopab  4131  nfopab1  4132  nfopab2  4133  repizf2  4225  nfdm  4944  fun11iun  5569  eusvobj2  5960  nfoprab1  6024  nfoprab2  6025  nfoprab3  6026  nfoprab  6027  nfrecs  6423  nffrec  6512  nfixpxy  6834  nfixp1  6835  nfwrd  11066