Theorem nfab 2905

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

Syntax hints:  Ⅎwnf 1785  {cab 2715  Ⅎwnfc 2884

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 2716  df-nfc 2886

This theorem is referenced by:  nfaba1OLD  2908  nfrabw  3427  nfunOLD  4112  sbcel12  4352  sbceqg  4353  nfpw  4561  nfpr  4637  nfint  4900  intab  4921  nfiun  4966  nfiin  4967  nfiu1OLD  4971  nfii1  4972  nfopab1  5156  nfopab2  5157  nfdm  5900  eusvobj2  7352  nfoprab1  7421  nfoprab2  7422  nfoprab3  7423  nfoprab  7424  fiun  7889  f1iun  7890  nffrecs  8226  nfixpw  8857  nfixp  8858  nfixp1  8859  reclem2pr  10962  nfwrd  14496  mreiincl  17549  lss1d  20949  iinabrex  32654  disjabrex  32667  disjabrexf  32668  esumc  34211  bnj900  35087  bnj1014  35119  bnj1123  35144  bnj1307  35181  bnj1398  35192  bnj1444  35201  bnj1445  35202  bnj1446  35203  bnj1447  35204  bnj1467  35212  bnj1518  35222  bnj1519  35223  fineqvrep  35274  dfon2lem3  35981  sdclem1  38078  heibor1  38145  dihglblem5  41758  permaxrep  45451  ssfiunibd  45760  hoidmvlelem1  47041  nfsetrecs  50173  setrec2lem2  50181  setrec2  50182