Theorem nfab1 2930

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

This proof depends on syntax axioms:  {cab 2744  Ⅎwnfc 2913

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 2179

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 2745  df-nfc 2915

This theorem is used by:  nfabd2  2951  eqabf  2957  abid2fOLD  2959  nfrab1  3439  elabgf  3636  nfsbc1d  3765  ss2ab  4018  ab0ALT  4340  euabsn  4697  iunab  5021  iinab  5037  zfrep4  5259  rnep  5922  sniota  6534  opabiotafun  6968  nfixp1  8925  scottabf  9878  scottexsOLD  9882  scott0bsOLD  9884  cp  9893  symgval  19472  ofpreima  33047  algextdeglem6  34143  qqhval2  34403  esum2dlem  34513  sigaclcu2  34541  bnj1366  35249  bnj1321  35447  bnj1384  35452  currysetlem  37622  currysetlem1  37624  bj-reabeq  37704  mptsnunlem  38025  topdifinffinlem  38034  compab  45192  permaxrep  45756  ssfiunibd  46069  absnsb  47805  setrec2lem2  50513