Theorem nfab1 2908

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

Syntax hints:  {cab 2715  Ⅎwnfc 2886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-10 2139

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-ex 1784  df-nf 1788  df-sb 2069  df-clab 2716  df-nfc 2888

This theorem is referenced by:  nfabd2  2932  abid2f  2938  abeq2f  2939  nfrab1  3310  elabgtOLD  3597  elabgf  3598  elabgOLD  3601  nfsbc1d  3729  ss2ab  3989  ab0ALT  4307  abn0OLD  4312  euabsn  4659  iunab  4977  iinab  4993  zfrep4  5215  rnep  5825  sniota  6409  opabiotafun  6831  nfixp1  8664  scottexs  9576  scott0s  9577  cp  9580  symgval  18891  ofpreima  30904  qqhval2  31832  esum2dlem  31960  sigaclcu2  31988  bnj1366  32709  bnj1321  32907  bnj1384  32912  currysetlem  35061  currysetlem1  35063  bj-reabeq  35144  mptsnunlem  35436  topdifinffinlem  35445  scottabf  41747  compab  41949  ssfiunibd  42738  absnsb  44408  setrec2lem2  46286