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

Theorem vsnid 4598
Description: A setvar variable is a member of its singleton. (Contributed by David A. Wheeler, 8-Dec-2018.)
Assertion
Ref Expression
vsnid 𝑥 ∈ {𝑥}

Proof of Theorem vsnid
StepHypRef Expression
1 vex 3502 . 2 𝑥 ∈ V
21snid 4597 1 𝑥 ∈ {𝑥}
Colors of variables: wff setvar class
Syntax hints:  wcel 2107  {csn 4563
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-v 3501  df-sn 4564
This theorem is referenced by:  exsnrex  4616  rext  5336  unipw  5338  xpdifid  6022  opabiota  6742  fnressn  6915  fressnfv  6917  snnex  7472  wfrlem14  7962  wfrlem16  7964  mapsnd  8442  findcard2d  8752  ac6sfi  8754  iunfi  8804  elirrv  9052  kmlem2  9569  fin1a2lem10  9823  hsmexlem4  9843  iunfo  9953  modfsummodslem1  15139  lcmfunsnlem2lem1  15974  coprmprod  15997  coprmproddvdslem  15998  lbsextlem4  19855  coe1fzgsumdlem  20386  evl1gsumdlem  20435  frlmlbs  20857  maducoeval2  21165  dishaus  21906  dis2ndc  21984  dislly  22021  dissnlocfin  22053  comppfsc  22056  txdis  22156  txdis1cn  22159  txkgen  22176  isufil2  22432  alexsubALTlem4  22574  tmdgsum  22619  dscopn  23098  ovolfiniun  24017  volfiniun  24063  jensen  25480  uvtx01vtx  27093  cplgr1vlem  27125  unidifsnel  30209  extdg1id  30939  esum2dlem  31237  bnj1498  32217  funen1cnv  32241  cvmlift2lem1  32433  frrlem12  33018  frrlem14  33020  funpartlem  33287  topdifinffinlem  34497  fvineqsneq  34562  pibt2  34567  finixpnum  34744  mbfresfi  34805  pclfinN  36903  mzpcompact2lem  39209  fourierdlem48  42301  sge0sup  42535  funressnvmo  43142  c0snmgmhm  44013
  Copyright terms: Public domain W3C validator