Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfab1 Structured version   Visualization version   GIF version

Theorem nfab1 2957
 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.
StepHypRef Expression
1 nfsab1 2785 . 2 𝑥 𝑦 ∈ {𝑥𝜑}
21nfci 2939 1 𝑥{𝑥𝜑}
 Colors of variables: wff setvar class Syntax hints:  {cab 2776  Ⅎwnfc 2936 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 1911  ax-6 1970  ax-7 2015  ax-10 2142 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-nfc 2938 This theorem is referenced by:  nfabd2  2978  abid2f  2984  abeq2f  2985  nfrab1  3337  elabgt  3609  elabgf  3610  elabg  3614  nfsbc1d  3738  ss2ab  3987  ab0  4287  abn0  4290  euabsn  4622  iunab  4939  iinab  4954  zfrep4  5165  rnep  5762  sniota  6316  opabiotafun  6720  nfixp1  8468  scottexs  9303  scott0s  9304  cp  9307  symgval  18493  ofpreima  30438  qqhval2  31348  esum2dlem  31476  sigaclcu2  31504  bnj1366  32226  bnj1321  32424  bnj1384  32429  currysetlem  34399  currysetlem1  34401  bj-reabeq  34482  mptsnunlem  34774  topdifinffinlem  34783  scottabf  40991  compab  41189  ssfiunibd  41984  absnsb  43662  setrec2lem2  45265
 Copyright terms: Public domain W3C validator