Theorem nfab 2378

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

Syntax hints:  Ⅎwnf 1508  {cab 2216  Ⅎwnfc 2360

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1810  df-clab 2217  df-nfc 2362

This theorem is referenced by:  nfaba1  2379  nfrabw  2713  sbcel12g  3141  sbceqg  3142  nfun  3362  nfpw  3666  nfpr  3720  nfop  3879  nfuni  3900  nfint  3939  intab  3958  nfiunxy  3997  nfiinxy  3998  nfiunya  3999  nfiinya  4000  nfiu1  4001  nfii1  4002  nfopab  4158  nfopab1  4159  nfopab2  4160  repizf2  4254  nfdm  4978  fun11iun  5607  eusvobj2  6009  nfoprab1  6075  nfoprab2  6076  nfoprab3  6077  nfoprab  6078  nfrecs  6478  nffrec  6567  nfixpxy  6891  nfixp1  6892  nfwrd  11151