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  7403  nfoprab1  7472  nfoprab2  7473  nfoprab3  7474  nfoprab  7475  fiun  7931  f1iun  7932  nffrecs  8270  nfwrecsOLD  8304  nfixpw  8912  nfixp  8913  nfixp1  8914  reclem2pr  11045  nfwrd  14495  mreiincl  17542  lss1d  20579  iinabrex  31838  disjabrex  31851  disjabrexf  31852  esumc  33118  bnj900  34009  bnj1014  34041  bnj1123  34066  bnj1307  34103  bnj1398  34114  bnj1444  34123  bnj1445  34124  bnj1446  34125  bnj1447  34126  bnj1467  34134  bnj1518  34144  bnj1519  34145  fineqvrep  34164  dfon2lem3  34832  sdclem1  36703  heibor1  36770  dihglblem5  40261  ssfiunibd  44104  hoidmvlelem1  45396  nfsetrecs  47815  setrec2lem2  47823  setrec2  47824