Theorem nfab 2904

Description: Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.) Add disjoint variable condition to avoid ax-13 2376. See nfabg 2905 for a less restrictive version requiring more axioms. (Revised by GG, 20-Jan-2024.)

Hypothesis

Ref	Expression
nfab.1	⊢ Ⅎ𝑥𝜑

Assertion

Ref	Expression
nfab	⊢ Ⅎ𝑥{𝑦 ∣ 𝜑}

Distinct variable group:   𝑥,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦)

Proof of Theorem nfab

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfab.1	. . 3 ⊢ Ⅎ𝑥𝜑
2	1	nfsab 2726	. 2 ⊢ Ⅎ𝑥 𝑧 ∈ {𝑦 ∣ 𝜑}
3	2	nfci 2886	1 ⊢ Ⅎ𝑥{𝑦 ∣ 𝜑}

Syntax hints:  Ⅎwnf 1785  {cab 2714  Ⅎwnfc 2883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-10 2147  ax-11 2163  ax-12 2185

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2715  df-nfc 2885

This theorem is referenced by:  nfaba1OLD  2907  nfrabw  3426  nfunOLD  4111  sbcel12  4351  sbceqg  4352  nfpw  4560  nfpr  4636  nfint  4899  intab  4920  nfiun  4965  nfiin  4966  nfiu1OLD  4970  nfii1  4971  nfopab1  5155  nfopab2  5156  nfdm  5906  eusvobj2  7359  nfoprab1  7428  nfoprab2  7429  nfoprab3  7430  nfoprab  7431  fiun  7896  f1iun  7897  nffrecs  8233  nfixpw  8864  nfixp  8865  nfixp1  8866  reclem2pr  10971  nfwrd  14505  mreiincl  17558  lss1d  20958  iinabrex  32639  disjabrex  32652  disjabrexf  32653  esumc  34195  bnj900  35071  bnj1014  35103  bnj1123  35128  bnj1307  35165  bnj1398  35176  bnj1444  35185  bnj1445  35186  bnj1446  35187  bnj1447  35188  bnj1467  35196  bnj1518  35206  bnj1519  35207  fineqvrep  35258  dfon2lem3  35965  sdclem1  38064  heibor1  38131  dihglblem5  41744  permaxrep  45433  ssfiunibd  45742  hoidmvlelem1  47023  nfsetrecs  50161  setrec2lem2  50169  setrec2  50170