Theorem nfab 2234

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

Syntax hints:  Ⅎwnf 1395  {cab 2075  Ⅎwnfc 2216

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 666  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-10 1442  ax-11 1443  ax-i12 1444  ax-bndl 1445  ax-4 1446  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474

This theorem depends on definitions:  df-bi 116  df-nf 1396  df-sb 1694  df-clab 2076  df-nfc 2218

This theorem is referenced by:  nfaba1  2235  nfrabxy  2548  sbcel12g  2947  sbceqg  2948  nfun  3157  nfpw  3446  nfpr  3496  nfop  3644  nfuni  3665  nfint  3704  intab  3723  nfiunxy  3762  nfiinxy  3763  nfiunya  3764  nfiinya  3765  nfiu1  3766  nfii1  3767  nfopab  3912  nfopab1  3913  nfopab2  3914  repizf2  4003  nfdm  4692  fun11iun  5287  eusvobj2  5652  nfoprab1  5712  nfoprab2  5713  nfoprab3  5714  nfoprab  5715  nfrecs  6086  nffrec  6175  nfixpxy  6488  nfixp1  6489