Theorem nfab1 2905

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 2720	. 2 ⊢ Ⅎ𝑥 𝑦 ∈ {𝑥 ∣ 𝜑}
2	1	nfci 2891	1 ⊢ Ⅎ𝑥{𝑥 ∣ 𝜑}

Syntax hints:  {cab 2712  Ⅎwnfc 2888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-10 2139

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1777  df-nf 1781  df-sb 2063  df-clab 2713  df-nfc 2890

This theorem is referenced by:  nfabd2  2927  eqabf  2933  abid2fOLD  2935  nfrab1  3454  elabgtOLDOLD  3674  elabgf  3675  elabgOLD  3678  nfsbc1d  3809  ss2ab  4072  ab0ALT  4387  euabsn  4731  iunab  5056  iinab  5073  zfrep4  5299  rnep  5940  sniota  6554  opabiotafun  6989  nfixp1  8957  scottexs  9925  scott0s  9926  cp  9929  symgval  19403  ofpreima  32682  algextdeglem6  33728  qqhval2  33945  esum2dlem  34073  sigaclcu2  34101  bnj1366  34822  bnj1321  35020  bnj1384  35025  currysetlem  36928  currysetlem1  36930  bj-reabeq  37010  mptsnunlem  37321  topdifinffinlem  37330  scottabf  44236  compab  44438  ssfiunibd  45260  absnsb  46977  setrec2lem2  48925