Theorem nfab1 2901

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 2887	1 ⊢ Ⅎ𝑥{𝑥 ∣ 𝜑}

Syntax hints:  {cab 2715  Ⅎwnfc 2884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-10 2147

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2716  df-nfc 2886

This theorem is referenced by:  nfabd2  2923  eqabf  2929  abid2fOLD  2931  nfrab1  3421  elabgf  3631  nfsbc1d  3760  ss2ab  4015  ab0ALT  4335  euabsn  4685  iunab  5009  iinab  5025  zfrep4  5240  rnep  5884  sniota  6491  opabiotafun  6922  nfixp1  8868  scottexs  9811  scott0s  9812  cp  9815  symgval  19312  ofpreima  32754  algextdeglem6  33899  qqhval2  34159  esum2dlem  34269  sigaclcu2  34297  bnj1366  35004  bnj1321  35202  bnj1384  35207  currysetlem  37187  currysetlem1  37189  bj-reabeq  37269  mptsnunlem  37587  topdifinffinlem  37596  scottabf  44590  compab  44791  permaxrep  45356  ssfiunibd  45665  absnsb  47381  setrec2lem2  50047