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 2370. 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 2726	. 2 ⊢ Ⅎ𝑥 𝑧 ∈ {𝑦 ∣ 𝜑}
3	2	nfci 2887	1 ⊢ Ⅎ𝑥{𝑦 ∣ 𝜑}

Syntax hints:  Ⅎwnf 1784  {cab 2713  Ⅎwnfc 2884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-10 2136  ax-11 2153  ax-12 2170

This theorem depends on definitions:  df-bi 206  df-ex 1781  df-nf 1785  df-sb 2067  df-clab 2714  df-nfc 2886

This theorem is referenced by:  nfaba1  2912  nfun  4112  sbcel12  4355  sbceqg  4356  nfpw  4566  nfpr  4638  nfint  4904  intab  4926  nfiun  4971  nfiin  4972  nfiu1  4975  nfii1  4976  nfopab1  5162  nfopab2  5163  nfdm  5892  eusvobj2  7329  nfoprab1  7398  nfoprab2  7399  nfoprab3  7400  nfoprab  7401  fiun  7853  f1iun  7854  nffrecs  8169  nfwrecsOLD  8203  nfixpw  8775  nfixp  8776  nfixp1  8777  reclem2pr  10905  nfwrd  14346  mreiincl  17402  lss1d  20331  iinabrex  31195  disjabrex  31208  disjabrexf  31209  esumc  32317  bnj900  33208  bnj1014  33240  bnj1123  33265  bnj1307  33302  bnj1398  33313  bnj1444  33322  bnj1445  33323  bnj1446  33324  bnj1447  33325  bnj1467  33333  bnj1518  33343  bnj1519  33344  fineqvrep  33363  dfon2lem3  34044  sdclem1  36006  heibor1  36073  dihglblem5  39566  ssfiunibd  43183  hoidmvlelem1  44470  nfsetrecs  46743  setrec2lem2  46751  setrec2  46752