MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ssnid Structured version   Unicode version

Theorem ssnid 3918
Description: A setvar variable is a member of its singleton (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
Assertion
Ref Expression
ssnid  |-  x  e. 
{ x }

Proof of Theorem ssnid
StepHypRef Expression
1 vex 2987 . 2  |-  x  e. 
_V
21snid 3917 1  |-  x  e. 
{ x }
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1756   {csn 3889
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-v 2986  df-sn 3890
This theorem is referenced by:  exsnrex  3926  rext  4552  unipw  4554  xpdifid  5278  opabiota  5766  fnressn  5906  fressnfv  5908  snnex  6394  ac6sfi  7568  iunfi  7611  elirrv  7824  kmlem2  8332  fin1a2lem10  8590  hsmexlem4  8610  iunfo  8715  fsumcom2  13253  lbsextlem4  17254  evl1gsumdlem  17802  frlmlbs  18237  dishaus  18998  dis2ndc  19076  dislly  19113  txdis  19217  txdis1cn  19220  txkgen  19237  isufil2  19493  alexsubALTlem4  19634  tmdgsum  19678  dscopn  20178  ovolfiniun  20996  volfiniun  21040  jensen  22394  cusgrares  23392  uvtx01vtx  23412  cvmlift2lem1  27203  fprodcom2  27507  wfrlem14  27749  wfrlem16  27751  funpartlem  27985  finixpnum  28426  mbfresfi  28450  comppfsc  28591  mzpcompact2lem  29100  modfsummodslem1  30252  fsumsplitsnun  30254  frgrancvvdeqlem3  30637  frgrancvvdeqlem4  30638  frgrawopreg1  30655  frgrawopreg2  30656  coe1fzgsumdlem  30849  bnj1498  32064  pclfinN  33556
  Copyright terms: Public domain W3C validator