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  3410  elabgf  3618  nfsbc1d  3747  ss2ab  4002  ab0ALT  4322  euabsn  4671  iunab  4995  iinab  5011  zfrep4  5228  rnep  5876  sniota  6483  opabiotafun  6914  nfixp1  8859  scottexs  9802  scott0s  9803  cp  9806  symgval  19337  ofpreima  32753  algextdeglem6  33882  qqhval2  34142  esum2dlem  34252  sigaclcu2  34280  bnj1366  34987  bnj1321  35185  bnj1384  35190  currysetlem  37268  currysetlem1  37270  bj-reabeq  37350  mptsnunlem  37668  topdifinffinlem  37677  scottabf  44685  compab  44886  permaxrep  45451  ssfiunibd  45760  absnsb  47487  setrec2lem2  50181