Theorem nfab 2905

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

Syntax hints:  Ⅎwnf 1785  {cab 2715  Ⅎwnfc 2884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-10 2147  ax-11 2163  ax-12 2185

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2716  df-nfc 2886

This theorem is referenced by:  nfaba1OLD  2908  nfunOLD  4125  sbcel12  4365  sbceqg  4366  nfpw  4575  nfpr  4651  nfint  4914  intab  4935  nfiun  4980  nfiin  4981  nfiu1OLD  4985  nfii1  4986  nfopab1  5170  nfopab2  5171  nfdm  5908  eusvobj2  7360  nfoprab1  7429  nfoprab2  7430  nfoprab3  7431  nfoprab  7432  fiun  7897  f1iun  7898  nffrecs  8235  nfixpw  8866  nfixp  8867  nfixp1  8868  reclem2pr  10971  nfwrd  14478  mreiincl  17527  lss1d  20926  iinabrex  32655  disjabrex  32668  disjabrexf  32669  esumc  34228  bnj900  35104  bnj1014  35136  bnj1123  35161  bnj1307  35198  bnj1398  35209  bnj1444  35218  bnj1445  35219  bnj1446  35220  bnj1447  35221  bnj1467  35229  bnj1518  35239  bnj1519  35240  fineqvrep  35289  dfon2lem3  35996  sdclem1  37988  heibor1  38055  dihglblem5  41668  permaxrep  45356  ssfiunibd  45665  hoidmvlelem1  46947  nfsetrecs  50039  setrec2lem2  50047  setrec2  50048