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  4124  sbcel12  4364  sbceqg  4365  nfpw  4572  nfpr  4646  nfint  4909  intab  4931  nfiun  4976  nfiin  4977  nfiu1OLD  4981  nfii1  4982  nfopab1  5165  nfopab2  5166  nfdm  5897  eusvobj2  7345  nfoprab1  7414  nfoprab2  7415  nfoprab3  7416  nfoprab  7417  fiun  7885  f1iun  7886  nffrecs  8223  nfixpw  8850  nfixp  8851  nfixp1  8852  reclem2pr  10961  nfwrd  14468  mreiincl  17516  lss1d  20884  iinabrex  32531  disjabrex  32544  disjabrexf  32545  esumc  34017  bnj900  34895  bnj1014  34927  bnj1123  34952  bnj1307  34989  bnj1398  35000  bnj1444  35009  bnj1445  35010  bnj1446  35011  bnj1447  35012  bnj1467  35020  bnj1518  35030  bnj1519  35031  fineqvrep  35069  dfon2lem3  35758  sdclem1  37722  heibor1  37789  dihglblem5  41277  permaxrep  44980  ssfiunibd  45291  hoidmvlelem1  46577  nfsetrecs  49672  setrec2lem2  49680  setrec2  49681