Theorem nfab 2901

Description: Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.) Add disjoint variable condition to avoid ax-13 2374. See nfabg 2902 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 2723	. 2 ⊢ Ⅎ𝑥 𝑧 ∈ {𝑦 ∣ 𝜑}
3	2	nfci 2883	1 ⊢ Ⅎ𝑥{𝑦 ∣ 𝜑}

Syntax hints:  Ⅎwnf 1784  {cab 2711  Ⅎwnfc 2880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-10 2146  ax-11 2162  ax-12 2182

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2712  df-nfc 2882

This theorem is referenced by:  nfaba1OLD  2904  nfunOLD  4120  sbcel12  4360  sbceqg  4361  nfpw  4568  nfpr  4644  nfint  4907  intab  4928  nfiun  4973  nfiin  4974  nfiu1OLD  4978  nfii1  4979  nfopab1  5163  nfopab2  5164  nfdm  5895  eusvobj2  7344  nfoprab1  7413  nfoprab2  7414  nfoprab3  7415  nfoprab  7416  fiun  7881  f1iun  7882  nffrecs  8219  nfixpw  8846  nfixp  8847  nfixp1  8848  reclem2pr  10946  nfwrd  14452  mreiincl  17500  lss1d  20898  iinabrex  32551  disjabrex  32564  disjabrexf  32565  esumc  34085  bnj900  34962  bnj1014  34994  bnj1123  35019  bnj1307  35056  bnj1398  35067  bnj1444  35076  bnj1445  35077  bnj1446  35078  bnj1447  35079  bnj1467  35087  bnj1518  35097  bnj1519  35098  fineqvrep  35158  dfon2lem3  35848  sdclem1  37803  heibor1  37870  dihglblem5  41417  permaxrep  45123  ssfiunibd  45434  hoidmvlelem1  46717  nfsetrecs  49811  setrec2lem2  49819  setrec2  49820