Theorem nfab 2932

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

This proof depends on syntax axioms:  Ⅎwnf 1816  {cab 2741  Ⅎwnfc 2911

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-10 2180  ax-11 2197  ax-12 2216

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-nf 1817  df-sb 2102  df-clab 2742  df-nfc 2913

This theorem is used by:  nfrabw  3451  sbcel12  4372  sbceqg  4373  nfpw  4580  nfpr  4653  nfint  4920  intab  4941  nfiun  4985  nfiin  4986  nfii1  4990  nfopab1  5179  nfopab2  5180  nfdm  5941  eusvobj2  7438  nfoprab1  7507  nfoprab2  7508  nfoprab3  7509  nfoprab  7510  fiun  7982  f1iun  7983  nffrecs  8332  nfixpw  8975  nfixp  8976  nfixp1  8977  setrec2lem2  10006  setrec2  10007  reclem2pr  11163  nfwrd  14718  mreiincl  17798  lss1d  21271  iinabrex  33238  disjabrex  33251  disjabrexf  33252  esumc  34766  bnj900  35642  bnj1014  35674  bnj1123  35699  bnj1307  35736  bnj1398  35747  bnj1444  35756  bnj1445  35757  bnj1446  35758  bnj1447  35759  bnj1467  35767  bnj1518  35777  bnj1519  35778  fineqvrep  35895  dfon2lem3  36738  sdclem1  38880  heibor1  38947  dihglblem5  42558  permaxrep  46202  ssfiunibd  46540  hoidmvlelem1  47820  nfsetrecs  51079