Theorem nfab 2910

Description: Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.) Add disjoint variable condition to avoid ax-13 2371. See nfabg 2911 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 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 2727	. 2 ⊢ Ⅎ𝑥 𝑧 ∈ {𝑦 ∣ 𝜑}
3	2	nfci 2887	1 ⊢ Ⅎ𝑥{𝑦 ∣ 𝜑}

Syntax hints:  Ⅎwnf 1791  {cab 2714  Ⅎwnfc 2884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-10 2141  ax-11 2158  ax-12 2175

This theorem depends on definitions:  df-bi 210  df-ex 1788  df-nf 1792  df-sb 2071  df-clab 2715  df-nfc 2886

This theorem is referenced by:  nfaba1  2912  nfun  4079  sbcel12  4323  sbceqg  4324  nfpw  4534  nfpr  4606  nfint  4869  intab  4889  nfiun  4934  nfiin  4935  nfiu1  4938  nfii1  4939  nfopab1  5123  nfopab2  5124  nfdm  5820  eusvobj2  7206  nfoprab1  7272  nfoprab2  7273  nfoprab3  7274  nfoprab  7275  fiun  7716  f1iun  7717  nffrecs  8025  nfwrecs  8049  nfixpw  8597  nfixp  8598  nfixp1  8599  reclem2pr  10662  nfwrd  14098  mreiincl  17099  lss1d  20000  iinabrex  30627  disjabrex  30640  disjabrexf  30641  esumc  31731  bnj900  32622  bnj1014  32654  bnj1123  32679  bnj1307  32716  bnj1398  32727  bnj1444  32736  bnj1445  32737  bnj1446  32738  bnj1447  32739  bnj1467  32747  bnj1518  32757  bnj1519  32758  fineqvrep  32777  dfon2lem3  33480  sdclem1  35638  heibor1  35705  dihglblem5  39049  ssfiunibd  42521  hoidmvlelem1  43808  nfsetrecs  46063  setrec2lem2  46071  setrec2  46072