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  4007  ab0ALT  4330  euabsn  4687  iunab  5010  iinab  5026  zfrep4  5246  rnep  5909  sniota  6530  opabiotafun  6966  nfixp1  8947  scottabf  9940  scottexsOLD  9944  scott0bsOLD  9946  cp  9955  setrec2lem2  9977  symgval  19586  ofpreima  33260  algextdeglem6  34355  qqhval2  34615  esum2dlem  34725  sigaclcu2  34753  bnj1366  35460  bnj1321  35658  bnj1384  35663  currysetlem  37859  currysetlem1  37861  bj-reabeq  37941  mptsnunlem  38263  topdifinffinlem  38272  compab  45426  permaxrep  45997  ssfiunibd  46326  absnsb  48098