Theorem nfab 2908

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

Syntax hints:  Ⅎwnf 1790  {cab 2718  Ⅎwnfc 2887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-10 2152  ax-11 2168  ax-12 2189

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-nf 1791  df-sb 2074  df-clab 2719  df-nfc 2889

This theorem is referenced by:  nfrabw  3429  sbcel12  4346  sbceqg  4347  nfpw  4555  nfpr  4631  nfint  4894  intab  4915  nfiun  4960  nfiin  4961  nfii1  4965  nfopab1  5149  nfopab2  5150  nfdm  5900  eusvobj2  7355  nfoprab1  7424  nfoprab2  7425  nfoprab3  7426  nfoprab  7427  fiun  7892  f1iun  7893  nffrecs  8230  nfixpw  8861  nfixp  8862  nfixp1  8863  reclem2pr  10969  nfwrd  14503  mreiincl  17556  lss1d  20960  iinabrex  32665  disjabrex  32678  disjabrexf  32679  esumc  34242  bnj900  35118  bnj1014  35150  bnj1123  35175  bnj1307  35212  bnj1398  35223  bnj1444  35232  bnj1445  35233  bnj1446  35234  bnj1447  35235  bnj1467  35243  bnj1518  35253  bnj1519  35254  fineqvrep  35302  dfon2lem3  36018  sdclem1  38117  heibor1  38184  dihglblem5  41797  permaxrep  45457  ssfiunibd  45764  hoidmvlelem1  47045  nfsetrecs  50183  setrec2lem2  50191  setrec2  50192