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 ⊢ Ⅎ𝑥{𝑦 ∣ 𝜑}

This proof depends on syntax axioms:  Ⅎwnf 1816  {cab 2739  Ⅎwnfc 2908

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-10 2178  ax-11 2194  ax-12 2213

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2740  df-nfc 2910

This theorem is used by:  nfrabw  3448  sbcel12  4369  sbceqg  4370  nfpw  4576  nfpr  4653  nfint  4917  intab  4938  nfiun  4982  nfiin  4983  nfii1  4987  nfopab1  5175  nfopab2  5176  nfdm  5933  eusvobj2  7404  nfoprab1  7473  nfoprab2  7474  nfoprab3  7475  nfoprab  7476  fiun  7944  f1iun  7945  nffrecs  8285  nfixpw  8928  nfixp  8929  nfixp1  8930  setrec2lem2  9957  setrec2  9958  reclem2pr  11114  nfwrd  14668  mreiincl  17746  lss1d  21218  iinabrex  33145  disjabrex  33158  disjabrexf  33159  esumc  34665  bnj900  35542  bnj1014  35574  bnj1123  35599  bnj1307  35636  bnj1398  35647  bnj1444  35656  bnj1445  35657  bnj1446  35658  bnj1447  35659  bnj1467  35667  bnj1518  35677  bnj1519  35678  fineqvrep  35755  dfon2lem3  36517  sdclem1  38645  heibor1  38712  dihglblem5  42323  permaxrep  45948  ssfiunibd  46268  hoidmvlelem1  47549  nfsetrecs  50733