Theorem nfab 2908

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

Syntax hints:  Ⅎwnf 1779  {cab 2711  Ⅎwnfc 2887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-10 2138  ax-11 2154  ax-12 2174

This theorem depends on definitions:  df-bi 207  df-ex 1776  df-nf 1780  df-sb 2062  df-clab 2712  df-nfc 2889

This theorem is referenced by:  nfaba1OLD  2911  nfunOLD  4180  sbcel12  4416  sbceqg  4417  nfpw  4623  nfpr  4696  nfint  4960  intab  4982  nfiun  5027  nfiin  5028  nfiu1OLD  5032  nfii1  5033  nfopab1  5217  nfopab2  5218  nfdm  5964  eusvobj2  7422  nfoprab1  7493  nfoprab2  7494  nfoprab3  7495  nfoprab  7496  fiun  7965  f1iun  7966  nffrecs  8306  nfwrecsOLD  8340  nfixpw  8954  nfixp  8955  nfixp1  8956  reclem2pr  11085  nfwrd  14577  mreiincl  17640  lss1d  20978  iinabrex  32588  disjabrex  32601  disjabrexf  32602  esumc  34031  bnj900  34921  bnj1014  34953  bnj1123  34978  bnj1307  35015  bnj1398  35026  bnj1444  35035  bnj1445  35036  bnj1446  35037  bnj1447  35038  bnj1467  35046  bnj1518  35056  bnj1519  35057  fineqvrep  35087  dfon2lem3  35766  sdclem1  37729  heibor1  37796  dihglblem5  41280  ssfiunibd  45259  hoidmvlelem1  46550  nfsetrecs  48916  setrec2lem2  48924  setrec2  48925