Theorem nfab1 2928

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

This proof depends on syntax axioms:  {cab 2741  Ⅎwnfc 2911

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-10 2180

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-nf 1817  df-sb 2102  df-clab 2742  df-nfc 2913

This theorem is used by:  nfabd2  2949  eqabf  2955  abid2fOLD  2957  nfrab1  3435  elabgf  3631  nfsbc1d  3760  ss2ab  3989  ab0ALT  4333  euabsn  4687  iunab  5013  iinab  5029  zfrep4  5250  rnep  5917  sniota  6552  opabiotafun  6991  nfixp1  8977  scottabf  9969  scottexsOLD  9973  scott0bsOLD  9975  cp  9984  setrec2lem2  10006  symgval  19618  ofpreima  33334  algextdeglem6  34437  qqhval2  34697  esum2dlem  34807  sigaclcu2  34835  bnj1366  35542  bnj1321  35740  bnj1384  35745  currysetlem  38049  currysetlem1  38051  bj-reabeq  38131  mptsnunlem  38466  topdifinffinlem  38475  compab  45627  permaxrep  46202  ssfiunibd  46540  absnsb  48312