Theorem nfab 2933

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

Syntax hints:  Ⅎwnf 1806  {cab 2743  Ⅎwnfc 2912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-10 2178  ax-11 2194  ax-12 2215

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-nf 1807  df-sb 2094  df-clab 2744  df-nfc 2914

This theorem is referenced by:  nfrabw  3454  sbcel12  4368  sbceqg  4369  nfpw  4577  nfpr  4654  nfint  4917  intab  4938  nfiun  4983  nfiin  4984  nfii1  4988  nfopab1  5174  nfopab2  5175  nfdm  5931  eusvobj2  7392  nfoprab1  7461  nfoprab2  7462  nfoprab3  7463  nfoprab  7464  fiun  7928  f1iun  7929  nffrecs  8268  nfixpw  8902  nfixp  8903  nfixp1  8904  reclem2pr  11021  nfwrd  14568  mreiincl  17636  lss1d  21050  iinabrex  32820  disjabrex  32833  disjabrexf  32834  esumc  34353  bnj900  35229  bnj1014  35261  bnj1123  35286  bnj1307  35323  bnj1398  35334  bnj1444  35343  bnj1445  35344  bnj1446  35345  bnj1447  35346  bnj1467  35354  bnj1518  35364  bnj1519  35365  fineqvrep  35417  dfon2lem3  36141  sdclem1  38249  heibor1  38316  dihglblem5  41929  permaxrep  45574  ssfiunibd  45887  hoidmvlelem1  47168  nfsetrecs  50316  setrec2lem2  50324  setrec2  50325