Theorem nfab 2911

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

Syntax hints:  Ⅎwnf 1783  {cab 2714  Ⅎwnfc 2890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-10 2141  ax-11 2157  ax-12 2177

This theorem depends on definitions:  df-bi 207  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2715  df-nfc 2892

This theorem is referenced by:  nfaba1OLD  2914  nfunOLD  4171  sbcel12  4411  sbceqg  4412  nfpw  4619  nfpr  4692  nfint  4956  intab  4978  nfiun  5023  nfiin  5024  nfiu1OLD  5028  nfii1  5029  nfopab1  5213  nfopab2  5214  nfdm  5962  eusvobj2  7423  nfoprab1  7494  nfoprab2  7495  nfoprab3  7496  nfoprab  7497  fiun  7967  f1iun  7968  nffrecs  8308  nfwrecsOLD  8342  nfixpw  8956  nfixp  8957  nfixp1  8958  reclem2pr  11088  nfwrd  14581  mreiincl  17639  lss1d  20961  iinabrex  32582  disjabrex  32595  disjabrexf  32596  esumc  34052  bnj900  34943  bnj1014  34975  bnj1123  35000  bnj1307  35037  bnj1398  35048  bnj1444  35057  bnj1445  35058  bnj1446  35059  bnj1447  35060  bnj1467  35068  bnj1518  35078  bnj1519  35079  fineqvrep  35109  dfon2lem3  35786  sdclem1  37750  heibor1  37817  dihglblem5  41300  ssfiunibd  45321  hoidmvlelem1  46610  nfsetrecs  49205  setrec2lem2  49213  setrec2  49214