Theorem nfab 2913

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 2914 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 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 2728	. 2 ⊢ Ⅎ𝑥 𝑧 ∈ {𝑦 ∣ 𝜑}
3	2	nfci 2890	1 ⊢ Ⅎ𝑥{𝑦 ∣ 𝜑}

Syntax hints:  Ⅎwnf 1786  {cab 2715  Ⅎwnfc 2887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-10 2137  ax-11 2154  ax-12 2171

This theorem depends on definitions:  df-bi 206  df-ex 1783  df-nf 1787  df-sb 2068  df-clab 2716  df-nfc 2889

This theorem is referenced by:  nfaba1  2915  nfun  4099  sbcel12  4342  sbceqg  4343  nfpw  4554  nfpr  4626  nfint  4889  intab  4909  nfiun  4954  nfiin  4955  nfiu1  4958  nfii1  4959  nfopab1  5144  nfopab2  5145  nfdm  5860  eusvobj2  7268  nfoprab1  7336  nfoprab2  7337  nfoprab3  7338  nfoprab  7339  fiun  7785  f1iun  7786  nffrecs  8099  nfwrecsOLD  8133  nfixpw  8704  nfixp  8705  nfixp1  8706  reclem2pr  10804  nfwrd  14246  mreiincl  17305  lss1d  20225  iinabrex  30908  disjabrex  30921  disjabrexf  30922  esumc  32019  bnj900  32909  bnj1014  32941  bnj1123  32966  bnj1307  33003  bnj1398  33014  bnj1444  33023  bnj1445  33024  bnj1446  33025  bnj1447  33026  bnj1467  33034  bnj1518  33044  bnj1519  33045  fineqvrep  33064  dfon2lem3  33761  sdclem1  35901  heibor1  35968  dihglblem5  39312  ssfiunibd  42848  hoidmvlelem1  44133  nfsetrecs  46392  setrec2lem2  46400  setrec2  46401