Theorem nfab 2912

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

Syntax hints:  Ⅎwnf 1787  {cab 2715  Ⅎwnfc 2886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-10 2139  ax-11 2156  ax-12 2173

This theorem depends on definitions:  df-bi 206  df-ex 1784  df-nf 1788  df-sb 2069  df-clab 2716  df-nfc 2888

This theorem is referenced by:  nfaba1  2914  nfun  4095  sbcel12  4339  sbceqg  4340  nfpw  4551  nfpr  4623  nfint  4886  intab  4906  nfiun  4951  nfiin  4952  nfiu1  4955  nfii1  4956  nfopab1  5140  nfopab2  5141  nfdm  5849  eusvobj2  7248  nfoprab1  7314  nfoprab2  7315  nfoprab3  7316  nfoprab  7317  fiun  7759  f1iun  7760  nffrecs  8070  nfwrecsOLD  8104  nfixpw  8662  nfixp  8663  nfixp1  8664  reclem2pr  10735  nfwrd  14174  mreiincl  17222  lss1d  20140  iinabrex  30809  disjabrex  30822  disjabrexf  30823  esumc  31919  bnj900  32809  bnj1014  32841  bnj1123  32866  bnj1307  32903  bnj1398  32914  bnj1444  32923  bnj1445  32924  bnj1446  32925  bnj1447  32926  bnj1467  32934  bnj1518  32944  bnj1519  32945  fineqvrep  32964  dfon2lem3  33667  sdclem1  35828  heibor1  35895  dihglblem5  39239  ssfiunibd  42738  hoidmvlelem1  44023  nfsetrecs  46278  setrec2lem2  46286  setrec2  46287