Theorem nfab1 2900

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

Syntax hints:  {cab 2714  Ⅎwnfc 2883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-10 2147

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2715  df-nfc 2885

This theorem is referenced by:  nfabd2  2922  eqabf  2928  abid2fOLD  2930  nfrab1  3409  elabgf  3617  nfsbc1d  3746  ss2ab  4001  ab0ALT  4321  euabsn  4670  iunab  4994  iinab  5010  zfrep4  5228  rnep  5882  sniota  6489  opabiotafun  6920  nfixp1  8866  scottexs  9811  scott0s  9812  cp  9815  symgval  19346  ofpreima  32738  algextdeglem6  33866  qqhval2  34126  esum2dlem  34236  sigaclcu2  34264  bnj1366  34971  bnj1321  35169  bnj1384  35174  currysetlem  37252  currysetlem1  37254  bj-reabeq  37334  mptsnunlem  37654  topdifinffinlem  37663  scottabf  44667  compab  44868  permaxrep  45433  ssfiunibd  45742  absnsb  47475  setrec2lem2  50169