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

Theorem ssnid 4056
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 3116 . 2  |-  x  e. 
_V
21snid 4055 1  |-  x  e. 
{ x }
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1767   {csn 4027
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-sn 4028
This theorem is referenced by:  exsnrex  4065  rext  4695  unipw  4697  xpdifid  5435  opabiota  5931  fnressn  6074  fressnfv  6076  snnex  6591  ac6sfi  7765  iunfi  7809  elirrv  8024  kmlem2  8532  fin1a2lem10  8790  hsmexlem4  8810  iunfo  8915  fsumsplitsnun  13536  fsumcom2  13555  modfsummodslem1  13572  lbsextlem4  17619  coe1fzgsumdlem  18154  evl1gsumdlem  18203  frlmlbs  18638  dishaus  19689  dis2ndc  19767  dislly  19804  dissnlocfin  19857  comppfsc  19860  txdis  19960  txdis1cn  19963  txkgen  19980  isufil2  20236  alexsubALTlem4  20377  tmdgsum  20421  dscopn  20921  ovolfiniun  21739  volfiniun  21784  jensen  23143  cusgrares  24245  uvtx01vtx  24265  frgrancvvdeqlem3  24806  frgrancvvdeqlem4  24807  frgrawopreg1  24824  frgrawopreg2  24825  cvmlift2lem1  28498  fprodcom2  28967  wfrlem14  29209  wfrlem16  29211  funpartlem  29445  finixpnum  29891  mbfresfi  29914  mzpcompact2lem  30515  fourierdlem48  31682  bnj1498  33413  pclfinN  34913
  Copyright terms: Public domain W3C validator