Theorem nfab1 2906

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

Syntax hints:  {cab 2714  Ⅎwnfc 2884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-10 2141

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-ex 1788  df-nf 1792  df-sb 2071  df-clab 2715  df-nfc 2886

This theorem is referenced by:  nfabd2  2930  abid2f  2936  abeq2f  2937  nfrab1  3296  elabgtOLD  3582  elabgf  3583  elabgOLD  3586  nfsbc1d  3712  ss2ab  3973  ab0ALT  4291  abn0OLD  4296  euabsn  4642  iunab  4960  iinab  4976  zfrep4  5189  rnep  5796  sniota  6371  opabiotafun  6792  nfixp1  8599  scottexs  9503  scott0s  9504  cp  9507  symgval  18761  ofpreima  30722  qqhval2  31644  esum2dlem  31772  sigaclcu2  31800  bnj1366  32522  bnj1321  32720  bnj1384  32725  currysetlem  34871  currysetlem1  34873  bj-reabeq  34954  mptsnunlem  35246  topdifinffinlem  35255  scottabf  41531  compab  41733  ssfiunibd  42521  absnsb  44193  setrec2lem2  46071