Theorem nfab 2929

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

Syntax hints:  Ⅎwnf 1802  {cab 2739  Ⅎwnfc 2908

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-10 2174  ax-11 2190  ax-12 2211

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-nf 1803  df-sb 2090  df-clab 2740  df-nfc 2910

This theorem is referenced by:  nfrabw  3450  sbcel12  4364  sbceqg  4365  nfpw  4573  nfpr  4650  nfint  4914  intab  4935  nfiun  4980  nfiin  4981  nfii1  4985  nfopab1  5169  nfopab2  5170  nfdm  5925  eusvobj2  7384  nfoprab1  7453  nfoprab2  7454  nfoprab3  7455  nfoprab  7456  fiun  7920  f1iun  7921  nffrecs  8259  nfixpw  8894  nfixp  8895  nfixp1  8896  reclem2pr  11003  nfwrd  14553  mreiincl  17607  lss1d  21010  iinabrex  32718  disjabrex  32731  disjabrexf  32732  esumc  34309  bnj900  35188  bnj1014  35220  bnj1123  35245  bnj1307  35282  bnj1398  35293  bnj1444  35302  bnj1445  35303  bnj1446  35304  bnj1447  35305  bnj1467  35313  bnj1518  35323  bnj1519  35324  fineqvrep  35374  dfon2lem3  36097  sdclem1  38206  heibor1  38273  dihglblem5  41886  permaxrep  45546  ssfiunibd  45852  hoidmvlelem1  47133  nfsetrecs  50271  setrec2lem2  50279  setrec2  50280