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

Theorem vsnid 4592
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 3495 . 2 𝑥 ∈ V
21snid 4591 1 𝑥 ∈ {𝑥}
Colors of variables: wff setvar class
Syntax hints:  wcel 2105  {csn 4557
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-v 3494  df-sn 4558
This theorem is referenced by:  exsnrex  4610  rext  5331  unipw  5333  xpdifid  6018  opabiota  6739  fnressn  6912  fressnfv  6914  snnex  7469  wfrlem14  7957  wfrlem16  7959  mapsnd  8438  findcard2d  8748  ac6sfi  8750  iunfi  8800  elirrv  9048  kmlem2  9565  fin1a2lem10  9819  hsmexlem4  9839  iunfo  9949  modfsummodslem1  15135  lcmfunsnlem2lem1  15970  coprmprod  15993  coprmproddvdslem  15994  lbsextlem4  19862  coe1fzgsumdlem  20397  evl1gsumdlem  20447  frlmlbs  20869  maducoeval2  21177  dishaus  21918  dis2ndc  21996  dislly  22033  dissnlocfin  22065  comppfsc  22068  txdis  22168  txdis1cn  22171  txkgen  22188  isufil2  22444  alexsubALTlem4  22586  tmdgsum  22631  dscopn  23110  ovolfiniun  24029  volfiniun  24075  jensen  25493  uvtx01vtx  27106  cplgr1vlem  27138  unidifsnel  30222  extdg1id  30952  esum2dlem  31250  bnj1498  32230  funen1cnv  32254  cvmlift2lem1  32446  frrlem12  33031  frrlem14  33033  funpartlem  33300  topdifinffinlem  34510  fvineqsneq  34575  pibt2  34580  finixpnum  34758  mbfresfi  34819  pclfinN  36916  mzpcompact2lem  39226  fourierdlem48  42316  sge0sup  42550  funressnvmo  43157  c0snmgmhm  44113
  Copyright terms: Public domain W3C validator