Theorem nfab 2928

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

This proof depends on syntax axioms:  Ⅎwnf 1815  {cab 2738  Ⅎwnfc 2907

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-10 2177  ax-11 2193  ax-12 2212

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-nf 1816  df-sb 2099  df-clab 2739  df-nfc 2909

This theorem is used by:  nfrabw  3447  sbcel12  4368  sbceqg  4369  nfpw  4576  nfpr  4649  nfint  4916  intab  4937  nfiun  4981  nfiin  4982  nfii1  4986  nfopab1  5174  nfopab2  5175  nfdm  5932  eusvobj2  7413  nfoprab1  7482  nfoprab2  7483  nfoprab3  7484  nfoprab  7485  fiun  7956  f1iun  7957  nffrecs  8305  nfixpw  8948  nfixp  8949  nfixp1  8950  setrec2lem2  9980  setrec2  9981  reclem2pr  11137  nfwrd  14692  mreiincl  17772  lss1d  21244  iinabrex  33211  disjabrex  33224  disjabrexf  33225  esumc  34730  bnj900  35606  bnj1014  35638  bnj1123  35663  bnj1307  35700  bnj1398  35711  bnj1444  35720  bnj1445  35721  bnj1446  35722  bnj1447  35723  bnj1467  35731  bnj1518  35741  bnj1519  35742  fineqvrep  35839  dfon2lem3  36640  sdclem1  38771  heibor1  38838  dihglblem5  42449  permaxrep  46090  ssfiunibd  46419  hoidmvlelem1  47699  nfsetrecs  50958