Theorem vsnid 4623

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 3448	. 2 ⊢ 𝑥 ∈ V
2	1	snid 4622	1 ⊢ 𝑥 ∈ {𝑥}

Syntax hints:   ∈ wcel 2109  {csn 4585

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-sn 4586

This theorem is referenced by:  exsnrex  4640  rext  5403  unipw  5405  xpdifid  6129  opabiota  6925  fnressn  7112  fressnfv  7114  snnex  7714  frrlem12  8253  frrlem14  8255  mapsnd  8836  findcard2d  9107  ac6sfi  9207  iunfi  9270  elirrvOLD  9526  kmlem2  10083  fin1a2lem10  10340  hsmexlem4  10360  iunfo  10470  modfsummodslem1  15735  lcmfunsnlem2lem1  16585  coprmprod  16608  coprmproddvdslem  16609  c0snmgmhm  20383  lbsextlem4  21104  frlmlbs  21740  coe1fzgsumdlem  22224  evl1gsumdlem  22277  maducoeval2  22561  dishaus  23303  dis2ndc  23381  dislly  23418  dissnlocfin  23450  comppfsc  23453  txdis  23553  txdis1cn  23556  txkgen  23573  isufil2  23829  alexsubALTlem4  23971  tmdgsum  24016  dscopn  24495  ovolfiniun  25436  volfiniun  25482  jensen  26933  uvtx01vtx  29378  cplgr1vlem  29410  unidifsnel  32515  gsumpart  33041  extdg1id  33655  irngss  33676  esum2dlem  34076  bnj1498  35045  funen1cnv  35072  wevgblacfn  35090  cvmlift2lem1  35283  funpartlem  35924  topdifinffinlem  37329  fvineqsneq  37394  pibt2  37399  finixpnum  37593  mbfresfi  37654  pclfinN  39888  sn-iotalem  42203  mzpcompact2lem  42733  dvmptfprod  45937  fourierdlem48  46146  sge0sup  46383  funressnvmo  47040  dfclnbgr6  47850  dfsclnbgr6  47852  termco  49464  termcarweu  49511  diag1f1o  49517  diag2f1o  49520