Theorem nfab1 2927

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

Syntax hints:  {cab 2741  Ⅎwnfc 2910

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-10 2176

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1810  df-nf 1814  df-sb 2097  df-clab 2742  df-nfc 2912

This theorem is referenced by:  nfabd2  2948  eqabf  2954  abid2fOLD  2956  nfrab1  3436  elabgf  3634  nfsbc1d  3763  ss2ab  4016  ab0ALT  4338  euabsn  4693  iunab  5017  iinab  5033  zfrep4  5255  rnep  5919  sniota  6529  opabiotafun  6963  nfixp1  8917  scottexs  9862  scott0s  9863  scottabf  9867  cp  9878  symgval  19442  ofpreima  32988  algextdeglem6  34090  qqhval2  34350  esum2dlem  34460  sigaclcu2  34488  bnj1366  35195  bnj1321  35393  bnj1384  35398  currysetlem  37559  currysetlem1  37561  bj-reabeq  37641  mptsnunlem  37962  topdifinffinlem  37971  compab  45131  permaxrep  45695  ssfiunibd  46008  absnsb  47741  setrec2lem2  50449