Theorem nfab 2898

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

Syntax hints:  Ⅎwnf 1778  {cab 2703  Ⅎwnfc 2876

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-10 2130  ax-11 2147  ax-12 2167

This theorem depends on definitions:  df-bi 206  df-ex 1775  df-nf 1779  df-sb 2061  df-clab 2704  df-nfc 2878

This theorem is referenced by:  nfaba1OLD  2901  nfunOLD  4163  sbcel12  4405  sbceqg  4406  nfpw  4616  nfpr  4689  nfint  4956  intab  4978  nfiun  5023  nfiin  5024  nfiu1OLD  5028  nfii1  5029  nfopab1  5215  nfopab2  5216  nfdm  5949  eusvobj2  7408  nfoprab1  7478  nfoprab2  7479  nfoprab3  7480  nfoprab  7481  fiun  7948  f1iun  7949  nffrecs  8290  nfwrecsOLD  8324  nfixpw  8937  nfixp  8938  nfixp1  8939  reclem2pr  11082  nfwrd  14546  mreiincl  17604  lss1d  20936  iinabrex  32489  disjabrex  32502  disjabrexf  32503  esumc  33897  bnj900  34787  bnj1014  34819  bnj1123  34844  bnj1307  34881  bnj1398  34892  bnj1444  34901  bnj1445  34902  bnj1446  34903  bnj1447  34904  bnj1467  34912  bnj1518  34922  bnj1519  34923  fineqvrep  34944  dfon2lem3  35622  sdclem1  37457  heibor1  37524  dihglblem5  41010  ssfiunibd  44960  hoidmvlelem1  46252  nfsetrecs  48468  setrec2lem2  48476  setrec2  48477