Theorem nfab 2344

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

Syntax hints:  Ⅎwnf 1474  {cab 2182  Ⅎwnfc 2326

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-nfc 2328

This theorem is referenced by:  nfaba1  2345  nfrabw  2678  sbcel12g  3099  sbceqg  3100  nfun  3320  nfpw  3619  nfpr  3673  nfop  3825  nfuni  3846  nfint  3885  intab  3904  nfiunxy  3943  nfiinxy  3944  nfiunya  3945  nfiinya  3946  nfiu1  3947  nfii1  3948  nfopab  4102  nfopab1  4103  nfopab2  4104  repizf2  4196  nfdm  4911  fun11iun  5528  eusvobj2  5911  nfoprab1  5975  nfoprab2  5976  nfoprab3  5977  nfoprab  5978  nfrecs  6374  nffrec  6463  nfixpxy  6785  nfixp1  6786  nfwrd  10980