Theorem nfab1 2909

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

Syntax hints:  {cab 2715  Ⅎwnfc 2887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-10 2137

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-ex 1783  df-nf 1787  df-sb 2068  df-clab 2716  df-nfc 2889

This theorem is referenced by:  nfabd2  2933  abid2f  2939  abeq2f  2940  nfrab1  3317  elabgtOLD  3604  elabgf  3605  elabgOLD  3608  nfsbc1d  3734  ss2ab  3993  ab0ALT  4310  abn0OLD  4315  euabsn  4662  iunab  4981  iinab  4997  zfrep4  5220  rnep  5836  sniota  6424  opabiotafun  6849  nfixp1  8706  scottexs  9645  scott0s  9646  cp  9649  symgval  18976  ofpreima  31002  qqhval2  31932  esum2dlem  32060  sigaclcu2  32088  bnj1366  32809  bnj1321  33007  bnj1384  33012  currysetlem  35134  currysetlem1  35136  bj-reabeq  35217  mptsnunlem  35509  topdifinffinlem  35518  scottabf  41858  compab  42060  ssfiunibd  42848  absnsb  44521  setrec2lem2  46400