Theorem nfab 2931

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

Syntax hints:  Ⅎwnf 1813  {cab 2741  Ⅎwnfc 2910

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-10 2176  ax-11 2192  ax-12 2213

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-nf 1814  df-sb 2097  df-clab 2742  df-nfc 2912

This theorem is referenced by:  nfrabw  3452  sbcel12  4377  sbceqg  4378  nfpw  4582  nfpr  4659  nfint  4923  intab  4944  nfiun  4989  nfiin  4990  nfii1  4994  nfopab1  5182  nfopab2  5183  nfdm  5943  eusvobj2  7404  nfoprab1  7473  nfoprab2  7474  nfoprab3  7475  nfoprab  7476  fiun  7941  f1iun  7942  nffrecs  8281  nfixpw  8915  nfixp  8916  nfixp1  8917  reclem2pr  11034  nfwrd  14582  mreiincl  17649  lss1d  21065  iinabrex  32895  disjabrex  32908  disjabrexf  32909  esumc  34422  bnj900  35298  bnj1014  35330  bnj1123  35355  bnj1307  35392  bnj1398  35403  bnj1444  35412  bnj1445  35413  bnj1446  35414  bnj1447  35415  bnj1467  35423  bnj1518  35433  bnj1519  35434  fineqvrep  35508  dfon2lem3  36256  sdclem1  38375  heibor1  38442  dihglblem5  42053  permaxrep  45698  ssfiunibd  46011  hoidmvlelem1  47292  nfsetrecs  50447  setrec2lem2  50455  setrec2  50456