Theorem nfab1 2926

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

This proof depends on syntax axioms:  {cab 2740  Ⅎwnfc 2909

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 2741  df-nfc 2911

This theorem is used by:  nfabd2  2947  eqabf  2953  abid2fOLD  2955  nfrab1  3434  elabgf  3631  nfsbc1d  3760  ss2ab  4012  ab0ALT  4333  euabsn  4690  iunab  5014  iinab  5030  zfrep4  5252  rnep  5915  sniota  6528  opabiotafun  6962  nfixp1  8929  scottabf  9882  scottexsOLD  9886  scott0bsOLD  9888  cp  9897  symgval  19504  ofpreima  33146  algextdeglem6  34240  qqhval2  34500  esum2dlem  34610  sigaclcu2  34638  bnj1366  35346  bnj1321  35544  bnj1384  35549  currysetlem  37697  currysetlem1  37699  bj-reabeq  37779  mptsnunlem  38100  topdifinffinlem  38109  compab  45273  permaxrep  45837  ssfiunibd  46150  absnsb  47923  setrec2lem2  50628