Theorem nfab 2909

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 2910 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 2722	. 2 ⊢ Ⅎ𝑥 𝑧 ∈ {𝑦 ∣ 𝜑}
3	2	nfci 2886	1 ⊢ Ⅎ𝑥{𝑦 ∣ 𝜑}

Syntax hints:  Ⅎwnf 1785  {cab 2709  Ⅎwnfc 2883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  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 1782  df-nf 1786  df-sb 2068  df-clab 2710  df-nfc 2885

This theorem is referenced by:  nfaba1  2911  nfun  4165  sbcel12  4408  sbceqg  4409  nfpw  4621  nfpr  4694  nfint  4960  intab  4982  nfiun  5027  nfiin  5028  nfiu1  5031  nfii1  5032  nfopab1  5218  nfopab2  5219  nfdm  5950  eusvobj2  7400  nfoprab1  7469  nfoprab2  7470  nfoprab3  7471  nfoprab  7472  fiun  7928  f1iun  7929  nffrecs  8267  nfwrecsOLD  8301  nfixpw  8909  nfixp  8910  nfixp1  8911  reclem2pr  11042  nfwrd  14492  mreiincl  17539  lss1d  20573  iinabrex  31795  disjabrex  31808  disjabrexf  31809  esumc  33044  bnj900  33935  bnj1014  33967  bnj1123  33992  bnj1307  34029  bnj1398  34040  bnj1444  34049  bnj1445  34050  bnj1446  34051  bnj1447  34052  bnj1467  34060  bnj1518  34070  bnj1519  34071  fineqvrep  34090  dfon2lem3  34752  sdclem1  36606  heibor1  36673  dihglblem5  40164  ssfiunibd  44009  hoidmvlelem1  45301  nfsetrecs  47721  setrec2lem2  47729  setrec2  47730