Theorem nfab 2930

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

This proof depends on syntax axioms:  Ⅎwnf 1816  {cab 2740  Ⅎwnfc 2909

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 1943  ax-6 2000  ax-7 2041  ax-10 2178  ax-11 2194  ax-12 2215

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2741  df-nfc 2911

This theorem is used by:  nfrabw  3450  sbcel12  4372  sbceqg  4373  nfpw  4579  nfpr  4656  nfint  4920  intab  4941  nfiun  4986  nfiin  4987  nfii1  4991  nfopab1  5179  nfopab2  5180  nfdm  5939  eusvobj2  7409  nfoprab1  7478  nfoprab2  7479  nfoprab3  7480  nfoprab  7481  fiun  7944  f1iun  7945  nffrecs  8286  nfixpw  8927  nfixp  8928  nfixp1  8929  reclem2pr  11061  nfwrd  14612  mreiincl  17686  lss1d  21153  iinabrex  33050  disjabrex  33063  disjabrexf  33064  esumc  34569  bnj900  35446  bnj1014  35478  bnj1123  35503  bnj1307  35540  bnj1398  35551  bnj1444  35560  bnj1445  35561  bnj1446  35562  bnj1447  35563  bnj1467  35571  bnj1518  35581  bnj1519  35582  fineqvrep  35648  dfon2lem3  36370  sdclem1  38501  heibor1  38568  dihglblem5  42179  permaxrep  45837  ssfiunibd  46150  hoidmvlelem1  47431  nfsetrecs  50620  setrec2lem2  50628  setrec2  50629