Theorem nfab1 2904

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

Syntax hints:  {cab 2718  Ⅎwnfc 2887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-10 2152

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-ex 1787  df-nf 1791  df-sb 2074  df-clab 2719  df-nfc 2889

This theorem is referenced by:  nfabd2  2925  eqabf  2931  abid2fOLD  2933  nfrab1  3412  elabgf  3619  nfsbc1d  3748  ss2ab  3999  ab0ALT  4316  euabsn  4665  iunab  4988  iinab  5004  zfrep4  5222  rnep  5876  sniota  6483  opabiotafun  6914  nfixp1  8863  scottexs  9809  scott0s  9810  cp  9813  symgval  19344  ofpreima  32764  algextdeglem6  33913  qqhval2  34173  esum2dlem  34283  sigaclcu2  34311  bnj1366  35018  bnj1321  35216  bnj1384  35221  currysetlem  37305  currysetlem1  37307  bj-reabeq  37387  mptsnunlem  37707  topdifinffinlem  37716  scottabf  44691  compab  44892  permaxrep  45457  ssfiunibd  45764  absnsb  47497  setrec2lem2  50191