Theorem nfab 2937

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

Syntax hints:  Ⅎwnf 1810  {cab 2747  Ⅎwnfc 2916

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-10 2182  ax-11 2198  ax-12 2219

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-nf 1811  df-sb 2098  df-clab 2748  df-nfc 2918

This theorem is referenced by:  nfrabw  3460  sbcel12  4382  sbceqg  4383  nfpw  4586  nfpr  4663  nfint  4926  intab  4947  nfiun  4992  nfiin  4993  nfii1  4997  nfopab1  5185  nfopab2  5186  nfdm  5942  eusvobj2  7403  nfoprab1  7472  nfoprab2  7473  nfoprab3  7474  nfoprab  7475  fiun  7939  f1iun  7940  nffrecs  8279  nfixpw  8913  nfixp  8914  nfixp1  8915  reclem2pr  11032  nfwrd  14579  mreiincl  17647  lss1d  21061  iinabrex  32854  disjabrex  32867  disjabrexf  32868  esumc  34385  bnj900  35261  bnj1014  35293  bnj1123  35318  bnj1307  35355  bnj1398  35366  bnj1444  35375  bnj1445  35376  bnj1446  35377  bnj1447  35378  bnj1467  35386  bnj1518  35396  bnj1519  35397  fineqvrep  35449  dfon2lem3  36173  sdclem1  38281  heibor1  38348  dihglblem5  41961  permaxrep  45606  ssfiunibd  45919  hoidmvlelem1  47200  nfsetrecs  50348  setrec2lem2  50356  setrec2  50357