Theorem nfab 2900

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

Syntax hints:  Ⅎwnf 1784  {cab 2709  Ⅎwnfc 2879

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-10 2144  ax-11 2160  ax-12 2180

This theorem depends on definitions:  df-bi 207  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2710  df-nfc 2881

This theorem is referenced by:  nfaba1OLD  2903  nfunOLD  4121  sbcel12  4361  sbceqg  4362  nfpw  4569  nfpr  4645  nfint  4907  intab  4928  nfiun  4973  nfiin  4974  nfiu1OLD  4978  nfii1  4979  nfopab1  5161  nfopab2  5162  nfdm  5891  eusvobj2  7338  nfoprab1  7407  nfoprab2  7408  nfoprab3  7409  nfoprab  7410  fiun  7875  f1iun  7876  nffrecs  8213  nfixpw  8840  nfixp  8841  nfixp1  8842  reclem2pr  10936  nfwrd  14447  mreiincl  17495  lss1d  20894  iinabrex  32544  disjabrex  32557  disjabrexf  32558  esumc  34059  bnj900  34936  bnj1014  34968  bnj1123  34993  bnj1307  35030  bnj1398  35041  bnj1444  35050  bnj1445  35051  bnj1446  35052  bnj1447  35053  bnj1467  35061  bnj1518  35071  bnj1519  35072  fineqvrep  35125  dfon2lem3  35818  sdclem1  37782  heibor1  37849  dihglblem5  41336  permaxrep  45038  ssfiunibd  45349  hoidmvlelem1  46632  nfsetrecs  49717  setrec2lem2  49725  setrec2  49726