Theorem nfab1 2901

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

Syntax hints:  {cab 2714  Ⅎwnfc 2884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-10 2142

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2715  df-nfc 2886

This theorem is referenced by:  nfabd2  2923  eqabf  2929  abid2fOLD  2931  nfrab1  3441  elabgf  3658  nfsbc1d  3788  ss2ab  4042  ab0ALT  4361  euabsn  4707  iunab  5032  iinab  5049  zfrep4  5268  rnep  5911  sniota  6527  opabiotafun  6964  nfixp1  8937  scottexs  9906  scott0s  9907  cp  9910  symgval  19357  ofpreima  32648  algextdeglem6  33761  qqhval2  34018  esum2dlem  34128  sigaclcu2  34156  bnj1366  34865  bnj1321  35063  bnj1384  35068  currysetlem  36968  currysetlem1  36970  bj-reabeq  37050  mptsnunlem  37361  topdifinffinlem  37370  scottabf  44231  compab  44433  permaxrep  44998  ssfiunibd  45305  absnsb  47023  setrec2lem2  49525