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

Syntax hints:  {cab 2710  Ⅎwnfc 2884

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 1914  ax-6 1972  ax-7 2012  ax-10 2138

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-nfc 2886

This theorem is referenced by:  nfabd2  2930  eqabf  2936  abid2fOLD  2938  nfrab1  3452  elabgtOLD  3664  elabgf  3665  elabgOLD  3668  nfsbc1d  3796  ss2ab  4057  ab0ALT  4377  abn0OLD  4382  euabsn  4731  iunab  5055  iinab  5072  zfrep4  5297  rnep  5927  sniota  6535  opabiotafun  6973  nfixp1  8912  scottexs  9882  scott0s  9883  cp  9886  symgval  19236  ofpreima  31890  qqhval2  32962  esum2dlem  33090  sigaclcu2  33118  bnj1366  33840  bnj1321  34038  bnj1384  34043  currysetlem  35826  currysetlem1  35828  bj-reabeq  35908  mptsnunlem  36219  topdifinffinlem  36228  scottabf  42999  compab  43201  ssfiunibd  44019  absnsb  45737  setrec2lem2  47739