Theorem nfab1 2910

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

Syntax hints:  {cab 2717  Ⅎwnfc 2893

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-10 2141

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-ex 1778  df-nf 1782  df-sb 2065  df-clab 2718  df-nfc 2895

This theorem is referenced by:  nfabd2  2935  eqabf  2941  abid2fOLD  2943  nfrab1  3464  elabgtOLDOLD  3687  elabgf  3688  elabgOLD  3691  nfsbc1d  3822  ss2ab  4085  ab0ALT  4404  euabsn  4751  iunab  5074  iinab  5091  zfrep4  5314  rnep  5951  sniota  6564  opabiotafun  7002  nfixp1  8976  scottexs  9956  scott0s  9957  cp  9960  symgval  19412  ofpreima  32683  algextdeglem6  33713  qqhval2  33928  esum2dlem  34056  sigaclcu2  34084  bnj1366  34805  bnj1321  35003  bnj1384  35008  currysetlem  36911  currysetlem1  36913  bj-reabeq  36993  mptsnunlem  37304  topdifinffinlem  37313  scottabf  44209  compab  44411  ssfiunibd  45224  absnsb  46942  setrec2lem2  48786