Theorem nfab1 2897

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

Syntax hints:  {cab 2711  Ⅎwnfc 2880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-10 2146

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2712  df-nfc 2882

This theorem is referenced by:  nfabd2  2919  eqabf  2925  abid2fOLD  2927  nfrab1  3416  elabgf  3626  nfsbc1d  3755  ss2ab  4010  ab0ALT  4330  euabsn  4678  iunab  5002  iinab  5018  zfrep4  5233  rnep  5871  sniota  6477  opabiotafun  6908  nfixp1  8848  scottexs  9787  scott0s  9788  cp  9791  symgval  19285  ofpreima  32649  algextdeglem6  33756  qqhval2  34016  esum2dlem  34126  sigaclcu2  34154  bnj1366  34862  bnj1321  35060  bnj1384  35065  currysetlem  37010  currysetlem1  37012  bj-reabeq  37092  mptsnunlem  37403  topdifinffinlem  37412  scottabf  44357  compab  44558  permaxrep  45123  ssfiunibd  45434  absnsb  47151  setrec2lem2  49819