Theorem nfab1 2925

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

Syntax hints:  {cab 2739  Ⅎwnfc 2908

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-10 2174

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-ex 1799  df-nf 1803  df-sb 2090  df-clab 2740  df-nfc 2910

This theorem is referenced by:  nfabd2  2946  eqabf  2952  abid2fOLD  2954  nfrab1  3433  elabgf  3633  nfsbc1d  3762  ss2ab  4014  ab0ALT  4333  euabsn  4684  iunab  5008  iinab  5024  zfrep4  5242  rnep  5901  sniota  6508  opabiotafun  6943  nfixp1  8896  scottexs  9842  scott0s  9843  cp  9846  symgval  19394  ofpreima  32817  algextdeglem6  33980  qqhval2  34240  esum2dlem  34350  sigaclcu2  34378  bnj1366  35088  bnj1321  35286  bnj1384  35291  currysetlem  37394  currysetlem1  37396  bj-reabeq  37476  mptsnunlem  37796  topdifinffinlem  37805  scottabf  44780  compab  44981  permaxrep  45546  ssfiunibd  45852  absnsb  47585  setrec2lem2  50279