Theorem nfab1 2925

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

This proof depends on syntax axioms:  {cab 2739  Ⅎwnfc 2908

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-10 2178

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2740  df-nfc 2910

This theorem is used by:  nfabd2  2946  eqabf  2952  abid2fOLD  2954  nfrab1  3432  elabgf  3628  nfsbc1d  3757  ss2ab  4009  ab0ALT  4330  euabsn  4687  iunab  5010  iinab  5026  zfrep4  5246  rnep  5909  sniota  6522  opabiotafun  6957  nfixp1  8930  scottabf  9920  scottexsOLD  9924  scott0bsOLD  9926  cp  9935  setrec2lem2  9957  symgval  19565  ofpreima  33241  algextdeglem6  34336  qqhval2  34596  esum2dlem  34706  sigaclcu2  34734  bnj1366  35442  bnj1321  35640  bnj1384  35645  currysetlem  37828  currysetlem1  37830  bj-reabeq  37910  mptsnunlem  38229  topdifinffinlem  38238  compab  45384  permaxrep  45948  ssfiunibd  46268  absnsb  48041