Theorem nfab 2898

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

Syntax hints:  Ⅎwnf 1783  {cab 2708  Ⅎwnfc 2877

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 2008  ax-10 2142  ax-11 2158  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2709  df-nfc 2879

This theorem is referenced by:  nfaba1OLD  2901  nfunOLD  4137  sbcel12  4377  sbceqg  4378  nfpw  4585  nfpr  4659  nfint  4923  intab  4945  nfiun  4990  nfiin  4991  nfiu1OLD  4995  nfii1  4996  nfopab1  5180  nfopab2  5181  nfdm  5918  eusvobj2  7382  nfoprab1  7453  nfoprab2  7454  nfoprab3  7455  nfoprab  7456  fiun  7924  f1iun  7925  nffrecs  8265  nfixpw  8892  nfixp  8893  nfixp1  8894  reclem2pr  11008  nfwrd  14515  mreiincl  17564  lss1d  20876  iinabrex  32505  disjabrex  32518  disjabrexf  32519  esumc  34048  bnj900  34926  bnj1014  34958  bnj1123  34983  bnj1307  35020  bnj1398  35031  bnj1444  35040  bnj1445  35041  bnj1446  35042  bnj1447  35043  bnj1467  35051  bnj1518  35061  bnj1519  35062  fineqvrep  35092  dfon2lem3  35780  sdclem1  37744  heibor1  37811  dihglblem5  41299  permaxrep  45003  ssfiunibd  45314  hoidmvlelem1  46600  nfsetrecs  49679  setrec2lem2  49687  setrec2  49688