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

Theorem vsnid 4242
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 3234 . 2 𝑥 ∈ V
21snid 4241 1 𝑥 ∈ {𝑥}
Colors of variables: wff setvar class
Syntax hints:  wcel 2030  {csn 4210
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-sn 4211
This theorem is referenced by:  exsnrex  4253  rext  4946  unipw  4948  xpdifid  5597  opabiota  6300  fnressn  6465  fressnfv  6467  snnex  7008  snnexOLD  7009  wfrlem14  7473  wfrlem16  7475  findcard2d  8243  ac6sfi  8245  iunfi  8295  elirrv  8542  kmlem2  9011  fin1a2lem10  9269  hsmexlem4  9289  iunfo  9399  fsumsplitsnunOLD  14530  fsumcom2OLD  14550  modfsummodslem1  14568  fprodcom2OLD  14759  lcmfunsnlem2lem1  15398  coprmprod  15422  coprmproddvdslem  15423  lbsextlem4  19209  coe1fzgsumdlem  19719  evl1gsumdlem  19768  frlmlbs  20184  maducoeval2  20494  dishaus  21234  dis2ndc  21311  dislly  21348  dissnlocfin  21380  comppfsc  21383  txdis  21483  txdis1cn  21486  txkgen  21503  isufil2  21759  alexsubALTlem4  21901  tmdgsum  21946  dscopn  22425  ovolfiniun  23315  volfiniun  23361  jensen  24760  uvtx01vtx  26346  uvtxa01vtx0OLD  26348  cplgr1vlem  26381  esum2dlem  30282  bnj1498  31255  cvmlift2lem1  31410  funpartlem  32174  topdifinffinlem  33325  finixpnum  33524  mbfresfi  33586  pclfinN  35504  mzpcompact2lem  37631  fourierdlem48  40689  sge0sup  40926  c0snmgmhm  42239
  Copyright terms: Public domain W3C validator