Theorem nfab1 2924

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

This proof depends on syntax axioms:  {cab 2738  Ⅎwnfc 2907

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-10 2177

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1812  df-nf 1816  df-sb 2099  df-clab 2739  df-nfc 2909

This theorem is used by:  nfabd2  2945  eqabf  2951  abid2fOLD  2953  nfrab1  3431  elabgf  3627  nfsbc1d  3756  ss2ab  3986  ab0ALT  4329  euabsn  4683  iunab  5009  iinab  5025  zfrep4  5245  rnep  5908  sniota  6529  opabiotafun  6965  nfixp1  8949  scottabf  9942  scottexsOLD  9946  scott0bsOLD  9948  cp  9957  setrec2lem2  9979  symgval  19590  ofpreima  33306  algextdeglem6  34400  qqhval2  34660  esum2dlem  34770  sigaclcu2  34798  bnj1366  35505  bnj1321  35703  bnj1384  35708  currysetlem  37950  currysetlem1  37952  bj-reabeq  38032  mptsnunlem  38354  topdifinffinlem  38363  compab  45518  permaxrep  46089  ssfiunibd  46418  absnsb  48190