Theorem nfab 2984

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

Syntax hints:  Ⅎwnf 1784  {cab 2799  Ⅎwnfc 2961

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 1911  ax-6 1970  ax-7 2015  ax-10 2145  ax-11 2161  ax-12 2177

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-nfc 2963

This theorem is referenced by:  nfaba1  2986  nfun  4141  sbcel12  4360  sbceqg  4361  nfpw  4560  nfpr  4628  nfint  4886  intab  4906  nfiun  4949  nfiin  4950  nfiu1  4953  nfii1  4954  nfopab  5134  nfopab1  5135  nfopab2  5136  nfdm  5823  eusvobj2  7149  nfoprab1  7215  nfoprab2  7216  nfoprab3  7217  nfoprab  7218  fiun  7644  f1iun  7645  nfwrecs  7949  nfixpw  8480  nfixp  8481  nfixp1  8482  reclem2pr  10470  nfwrd  13894  mreiincl  16867  lss1d  19735  disjabrex  30332  disjabrexf  30333  esumc  31310  bnj900  32201  bnj1014  32233  bnj1123  32258  bnj1307  32295  bnj1398  32306  bnj1444  32315  bnj1445  32316  bnj1446  32317  bnj1447  32318  bnj1467  32326  bnj1518  32336  bnj1519  32337  dfon2lem3  33030  nffrecs  33120  sdclem1  35033  heibor1  35103  dihglblem5  38449  ssfiunibd  41596  hoidmvlelem1  42897  nfsetrecs  44809  setrec2lem2  44817  setrec2  44818