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  3319  nfpw  3618  nfpr  3672  nfop  3824  nfuni  3845  nfint  3884  intab  3903  nfiunxy  3942  nfiinxy  3943  nfiunya  3944  nfiinya  3945  nfiu1  3946  nfii1  3947  nfopab  4101  nfopab1  4102  nfopab2  4103  repizf2  4195  nfdm  4910  fun11iun  5525  eusvobj2  5908  nfoprab1  5971  nfoprab2  5972  nfoprab3  5973  nfoprab  5974  nfrecs  6365  nffrec  6454  nfixpxy  6776  nfixp1  6777  nfwrd  10963