Theorem nfab1 2929

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

Syntax hints:  {cab 2743  Ⅎwnfc 2912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-10 2178

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1803  df-nf 1807  df-sb 2094  df-clab 2744  df-nfc 2914

This theorem is referenced by:  nfabd2  2950  eqabf  2956  abid2fOLD  2958  nfrab1  3437  elabgf  3636  nfsbc1d  3765  ss2ab  4017  ab0ALT  4337  euabsn  4688  iunab  5012  iinab  5028  zfrep4  5248  rnep  5908  sniota  6516  opabiotafun  6951  nfixp1  8904  scottexs  9849  scott0s  9850  scottabf  9854  cp  9865  symgval  19432  ofpreima  32922  algextdeglem6  34029  qqhval2  34289  esum2dlem  34399  sigaclcu2  34427  bnj1366  35134  bnj1321  35332  bnj1384  35337  currysetlem  37442  currysetlem1  37444  bj-reabeq  37524  mptsnunlem  37844  topdifinffinlem  37853  compab  45015  permaxrep  45580  ssfiunibd  45886  absnsb  47619  setrec2lem2  50323