Theorem nfab1 2896

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

Syntax hints:  {cab 2709  Ⅎwnfc 2879

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 2144

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 2710  df-nfc 2881

This theorem is referenced by:  nfabd2  2918  eqabf  2924  abid2fOLD  2926  nfrab1  3415  elabgf  3630  nfsbc1d  3759  ss2ab  4013  ab0ALT  4331  euabsn  4679  iunab  5000  iinab  5016  zfrep4  5231  rnep  5867  sniota  6472  opabiotafun  6902  nfixp1  8842  scottexs  9777  scott0s  9778  cp  9781  symgval  19281  ofpreima  32642  algextdeglem6  33730  qqhval2  33990  esum2dlem  34100  sigaclcu2  34128  bnj1366  34836  bnj1321  35034  bnj1384  35039  currysetlem  36978  currysetlem1  36980  bj-reabeq  37060  mptsnunlem  37371  topdifinffinlem  37380  scottabf  44272  compab  44473  permaxrep  45038  ssfiunibd  45349  absnsb  47057  setrec2lem2  49725