Theorem nfab 2904

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

Syntax hints:  Ⅎwnf 1784  {cab 2714  Ⅎwnfc 2883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-10 2146  ax-11 2162  ax-12 2184

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2715  df-nfc 2885

This theorem is referenced by:  nfaba1OLD  2907  nfunOLD  4123  sbcel12  4363  sbceqg  4364  nfpw  4573  nfpr  4649  nfint  4912  intab  4933  nfiun  4978  nfiin  4979  nfiu1OLD  4983  nfii1  4984  nfopab1  5168  nfopab2  5169  nfdm  5900  eusvobj2  7350  nfoprab1  7419  nfoprab2  7420  nfoprab3  7421  nfoprab  7422  fiun  7887  f1iun  7888  nffrecs  8225  nfixpw  8854  nfixp  8855  nfixp1  8856  reclem2pr  10959  nfwrd  14466  mreiincl  17515  lss1d  20914  iinabrex  32644  disjabrex  32657  disjabrexf  32658  esumc  34208  bnj900  35085  bnj1014  35117  bnj1123  35142  bnj1307  35179  bnj1398  35190  bnj1444  35199  bnj1445  35200  bnj1446  35201  bnj1447  35202  bnj1467  35210  bnj1518  35220  bnj1519  35221  fineqvrep  35270  dfon2lem3  35977  sdclem1  37940  heibor1  38007  dihglblem5  41554  permaxrep  45243  ssfiunibd  45553  hoidmvlelem1  46835  nfsetrecs  49927  setrec2lem2  49935  setrec2  49936