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  4136  sbcel12  4376  sbceqg  4377  nfpw  4584  nfpr  4658  nfint  4922  intab  4944  nfiun  4989  nfiin  4990  nfiu1OLD  4994  nfii1  4995  nfopab1  5179  nfopab2  5180  nfdm  5917  eusvobj2  7381  nfoprab1  7452  nfoprab2  7453  nfoprab3  7454  nfoprab  7455  fiun  7923  f1iun  7924  nffrecs  8264  nfixpw  8891  nfixp  8892  nfixp1  8893  reclem2pr  11007  nfwrd  14514  mreiincl  17563  lss1d  20875  iinabrex  32504  disjabrex  32517  disjabrexf  32518  esumc  34047  bnj900  34925  bnj1014  34957  bnj1123  34982  bnj1307  35019  bnj1398  35030  bnj1444  35039  bnj1445  35040  bnj1446  35041  bnj1447  35042  bnj1467  35050  bnj1518  35060  bnj1519  35061  fineqvrep  35091  dfon2lem3  35768  sdclem1  37732  heibor1  37799  dihglblem5  41287  permaxrep  44989  ssfiunibd  45300  hoidmvlelem1  46586  nfsetrecs  49652  setrec2lem2  49660  setrec2  49661