Theorem nfab1 2893

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

Syntax hints:  {cab 2707  Ⅎwnfc 2876

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 2708  df-nfc 2878

This theorem is referenced by:  nfabd2  2915  eqabf  2921  abid2fOLD  2923  nfrab1  3417  elabgf  3632  nfsbc1d  3762  ss2ab  4016  ab0ALT  4334  euabsn  4680  iunab  5003  iinab  5020  zfrep4  5235  rnep  5873  sniota  6477  opabiotafun  6907  nfixp1  8852  scottexs  9802  scott0s  9803  cp  9806  symgval  19268  ofpreima  32622  algextdeglem6  33688  qqhval2  33948  esum2dlem  34058  sigaclcu2  34086  bnj1366  34795  bnj1321  34993  bnj1384  34998  currysetlem  36918  currysetlem1  36920  bj-reabeq  37000  mptsnunlem  37311  topdifinffinlem  37320  scottabf  44213  compab  44415  permaxrep  44980  ssfiunibd  45291  absnsb  47012  setrec2lem2  49680