Theorem nfab1 2900

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 2886	1 ⊢ Ⅎ𝑥{𝑥 ∣ 𝜑}

Syntax hints:  {cab 2714  Ⅎwnfc 2883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-10 2146

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2715  df-nfc 2885

This theorem is referenced by:  nfabd2  2922  eqabf  2928  abid2fOLD  2930  nfrab1  3419  elabgf  3629  nfsbc1d  3758  ss2ab  4013  ab0ALT  4333  euabsn  4683  iunab  5007  iinab  5023  zfrep4  5238  rnep  5876  sniota  6483  opabiotafun  6914  nfixp1  8856  scottexs  9799  scott0s  9800  cp  9803  symgval  19300  ofpreima  32743  algextdeglem6  33879  qqhval2  34139  esum2dlem  34249  sigaclcu2  34277  bnj1366  34985  bnj1321  35183  bnj1384  35188  currysetlem  37146  currysetlem1  37148  bj-reabeq  37228  mptsnunlem  37539  topdifinffinlem  37548  scottabf  44477  compab  44678  permaxrep  45243  ssfiunibd  45553  absnsb  47269  setrec2lem2  49935