Theorem vsnid 4632

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

Step	Hyp	Ref	Expression
1		vex 3465	. 2 ⊢ 𝑥 ∈ V
2	1	snid 4631	1 ⊢ 𝑥 ∈ {𝑥}

Syntax hints:   ∈ wcel 2149  {csn 4592

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3463  df-sn 4593

This theorem is referenced by:  exsnrex  4649  rext  5430  unipw  5432  xpdifid  6166  xpdifcnvepel  6167  opabiota  6964  fnressn  7156  fressnfv  7158  snnex  7757  frrlem12  8294  frrlem14  8296  mapsnd  8884  findcard2d  9151  ac6sfi  9244  iunfi  9300  elirrvOLDOLD  9561  kmlem2  10135  fin1a2lem10  10393  hsmexlem4  10413  iunfo  10523  modfsummodslem1  15844  lcmfunsnlem2lem1  16696  coprmprod  16719  coprmproddvdslem  16720  c0snmgmhm  20544  lbsextlem4  21263  frlmlbs  21916  coe1fzgsumdlem  22432  evl1gsumdlem  22485  maducoeval2  22766  dishaus  23508  dis2ndc  23586  dislly  23623  dissnlocfin  23655  comppfsc  23658  txdis  23758  txdis1cn  23761  txkgen  23778  isufil2  24034  alexsubALTlem4  24176  tmdgsum  24221  dscopn  24699  ovolfiniun  25629  volfiniun  25675  jensen  27119  uvtx01vtx  29688  cplgr1vlem  29720  unidifsnel  32822  gsumpart  33324  dflring3  33732  mplidomlem  33862  vieta  33915  extdg1id  34001  irngss  34022  esum2dlem  34427  bnj1498  35394  funen1cnv  35420  fineqvnttrclselem2  35468  wevgblacfn  35528  cvmlift2lem1  35727  funpartlem  36367  ttcid  36926  topdifinffinlem  37916  fvineqsneq  37981  pibt2  37986  finixpnum  38179  mbfresfi  38240  pclfinN  40599  sn-iotalem  42917  mzpcompact2lem  43409  dvmptfprod  46586  fourierdlem48  46795  sge0sup  47032  funressnvmo  47706  dfclnbgr6  48545  dfsclnbgr6  48547  termco  50179  termcarweu  50226  diag1f1o  50232  diag2f1o  50235