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

Syntax hints:  Ⅎwnf 1783  {cab 2713  Ⅎwnfc 2883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-10 2141  ax-11 2157  ax-12 2177

This theorem depends on definitions:  df-bi 207  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2714  df-nfc 2885

This theorem is referenced by:  nfaba1OLD  2907  nfunOLD  4146  sbcel12  4386  sbceqg  4387  nfpw  4594  nfpr  4668  nfint  4932  intab  4954  nfiun  4999  nfiin  5000  nfiu1OLD  5004  nfii1  5005  nfopab1  5189  nfopab2  5190  nfdm  5931  eusvobj2  7397  nfoprab1  7468  nfoprab2  7469  nfoprab3  7470  nfoprab  7471  fiun  7941  f1iun  7942  nffrecs  8282  nfwrecsOLD  8316  nfixpw  8930  nfixp  8931  nfixp1  8932  reclem2pr  11062  nfwrd  14561  mreiincl  17608  lss1d  20920  iinabrex  32550  disjabrex  32563  disjabrexf  32564  esumc  34082  bnj900  34960  bnj1014  34992  bnj1123  35017  bnj1307  35054  bnj1398  35065  bnj1444  35074  bnj1445  35075  bnj1446  35076  bnj1447  35077  bnj1467  35085  bnj1518  35095  bnj1519  35096  fineqvrep  35126  dfon2lem3  35803  sdclem1  37767  heibor1  37834  dihglblem5  41317  permaxrep  45031  ssfiunibd  45338  hoidmvlelem1  46624  nfsetrecs  49550  setrec2lem2  49558  setrec2  49559