Theorem nfab 2914

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

Syntax hints:  Ⅎwnf 1781  {cab 2717  Ⅎwnfc 2893

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-10 2141  ax-11 2158  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-ex 1778  df-nf 1782  df-sb 2065  df-clab 2718  df-nfc 2895

This theorem is referenced by:  nfaba1OLD  2917  nfunOLD  4194  sbcel12  4434  sbceqg  4435  nfpw  4641  nfpr  4715  nfint  4980  intab  5002  nfiun  5046  nfiin  5047  nfiu1OLD  5051  nfii1  5052  nfopab1  5236  nfopab2  5237  nfdm  5976  eusvobj2  7440  nfoprab1  7511  nfoprab2  7512  nfoprab3  7513  nfoprab  7514  fiun  7983  f1iun  7984  nffrecs  8324  nfwrecsOLD  8358  nfixpw  8974  nfixp  8975  nfixp1  8976  reclem2pr  11117  nfwrd  14591  mreiincl  17654  lss1d  20984  iinabrex  32591  disjabrex  32604  disjabrexf  32605  esumc  34015  bnj900  34905  bnj1014  34937  bnj1123  34962  bnj1307  34999  bnj1398  35010  bnj1444  35019  bnj1445  35020  bnj1446  35021  bnj1447  35022  bnj1467  35030  bnj1518  35040  bnj1519  35041  fineqvrep  35071  dfon2lem3  35749  sdclem1  37703  heibor1  37770  dihglblem5  41255  ssfiunibd  45224  hoidmvlelem1  46516  nfsetrecs  48778  setrec2lem2  48786  setrec2  48787