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

Theorem vsnid 4621
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 3447 . 2 𝑥 ∈ V
21snid 4620 1 𝑥 ∈ {𝑥}
Colors of variables: wff setvar class
Syntax hints:  wcel 2106  {csn 4584
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3445  df-sn 4585
This theorem is referenced by:  exsnrex  4639  rext  5403  unipw  5405  xpdifid  6118  opabiota  6921  fnressn  7100  fressnfv  7102  snnex  7688  frrlem12  8224  frrlem14  8226  wfrlem14OLD  8264  wfrlem16OLD  8266  mapsnd  8820  findcard2d  9106  ac6sfi  9227  iunfi  9280  elirrv  9528  kmlem2  10083  fin1a2lem10  10341  hsmexlem4  10361  iunfo  10471  modfsummodslem1  15669  lcmfunsnlem2lem1  16506  coprmprod  16529  coprmproddvdslem  16530  lbsextlem4  20607  frlmlbs  21188  coe1fzgsumdlem  21656  evl1gsumdlem  21706  maducoeval2  21973  dishaus  22717  dis2ndc  22795  dislly  22832  dissnlocfin  22864  comppfsc  22867  txdis  22967  txdis1cn  22970  txkgen  22987  isufil2  23243  alexsubALTlem4  23385  tmdgsum  23430  dscopn  23913  ovolfiniun  24849  volfiniun  24895  jensen  26322  uvtx01vtx  28231  cplgr1vlem  28263  unidifsnel  31348  gsumpart  31780  extdg1id  32229  irngss  32238  esum2dlem  32560  bnj1498  33542  funen1cnv  33561  cvmlift2lem1  33765  funpartlem  34494  topdifinffinlem  35785  fvineqsneq  35850  pibt2  35855  finixpnum  36030  mbfresfi  36091  pclfinN  38330  sn-iotalem  40609  mzpcompact2lem  41012  fourierdlem48  44327  sge0sup  44564  funressnvmo  45211  c0snmgmhm  46144
  Copyright terms: Public domain W3C validator