Theorem nfab 2934

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

This proof depends on syntax axioms:  Ⅎwnf 1816  {cab 2744  Ⅎwnfc 2913

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 2179  ax-11 2195  ax-12 2216

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

This theorem is used by:  nfrabw  3455  sbcel12  4379  sbceqg  4380  nfpw  4586  nfpr  4663  nfint  4927  intab  4948  nfiun  4993  nfiin  4994  nfii1  4998  nfopab1  5186  nfopab2  5187  nfdm  5946  eusvobj2  7415  nfoprab1  7484  nfoprab2  7485  nfoprab3  7486  nfoprab  7487  fiun  7949  f1iun  7950  nffrecs  8289  nfixpw  8923  nfixp  8924  nfixp1  8925  reclem2pr  11051  nfwrd  14600  mreiincl  17673  lss1d  21121  iinabrex  32951  disjabrex  32964  disjabrexf  32965  esumc  34472  bnj900  35349  bnj1014  35381  bnj1123  35406  bnj1307  35443  bnj1398  35454  bnj1444  35463  bnj1445  35464  bnj1446  35465  bnj1447  35466  bnj1467  35474  bnj1518  35484  bnj1519  35485  fineqvrep  35551  dfon2lem3  36296  sdclem1  38435  heibor1  38502  dihglblem5  42113  permaxrep  45756  ssfiunibd  46069  hoidmvlelem1  47350  nfsetrecs  50505  setrec2lem2  50513  setrec2  50514