Theorem nfab 2897

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 2898 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 2719	. 2 ⊢ Ⅎ𝑥 𝑧 ∈ {𝑦 ∣ 𝜑}
3	2	nfci 2879	1 ⊢ Ⅎ𝑥{𝑦 ∣ 𝜑}

Syntax hints:  Ⅎwnf 1783  {cab 2707  Ⅎwnfc 2876

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-10 2142  ax-11 2158  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-nfc 2878

This theorem is referenced by:  nfaba1OLD  2900  nfunOLD  4134  sbcel12  4374  sbceqg  4375  nfpw  4582  nfpr  4656  nfint  4920  intab  4942  nfiun  4987  nfiin  4988  nfiu1OLD  4992  nfii1  4993  nfopab1  5177  nfopab2  5178  nfdm  5915  eusvobj2  7379  nfoprab1  7450  nfoprab2  7451  nfoprab3  7452  nfoprab  7453  fiun  7921  f1iun  7922  nffrecs  8262  nfixpw  8889  nfixp  8890  nfixp1  8891  reclem2pr  11001  nfwrd  14508  mreiincl  17557  lss1d  20869  iinabrex  32498  disjabrex  32511  disjabrexf  32512  esumc  34041  bnj900  34919  bnj1014  34951  bnj1123  34976  bnj1307  35013  bnj1398  35024  bnj1444  35033  bnj1445  35034  bnj1446  35035  bnj1447  35036  bnj1467  35044  bnj1518  35054  bnj1519  35055  fineqvrep  35085  dfon2lem3  35773  sdclem1  37737  heibor1  37804  dihglblem5  41292  permaxrep  44996  ssfiunibd  45307  hoidmvlelem1  46593  nfsetrecs  49675  setrec2lem2  49683  setrec2  49684