Theorem nfab1 2893

Description: Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.)

Assertion

Ref	Expression
nfab1	⊢ Ⅎ𝑥{𝑥 ∣ 𝜑}

Proof of Theorem nfab1

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfsab1 2715	. 2 ⊢ Ⅎ𝑥 𝑦 ∈ {𝑥 ∣ 𝜑}
2	1	nfci 2879	1 ⊢ Ⅎ𝑥{𝑥 ∣ 𝜑}

Syntax hints:  {cab 2707  Ⅎwnfc 2876

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 2008  ax-10 2142

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-nfc 2878

This theorem is referenced by:  nfabd2  2915  eqabf  2921  abid2fOLD  2923  nfrab1  3426  elabgf  3641  nfsbc1d  3771  ss2ab  4025  ab0ALT  4344  euabsn  4690  iunab  5015  iinab  5032  zfrep4  5248  rnep  5890  sniota  6502  opabiotafun  6941  nfixp1  8891  scottexs  9840  scott0s  9841  cp  9844  symgval  19301  ofpreima  32589  algextdeglem6  33712  qqhval2  33972  esum2dlem  34082  sigaclcu2  34110  bnj1366  34819  bnj1321  35017  bnj1384  35022  currysetlem  36933  currysetlem1  36935  bj-reabeq  37015  mptsnunlem  37326  topdifinffinlem  37335  scottabf  44229  compab  44431  permaxrep  44996  ssfiunibd  45307  absnsb  47028  setrec2lem2  49683