Theorem vsnid 4639

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

Syntax hints:   ∈ wcel 2108  {csn 4601

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-sn 4602

This theorem is referenced by:  exsnrex  4656  rext  5423  unipw  5425  xpdifid  6157  opabiota  6961  fnressn  7148  fressnfv  7150  snnex  7752  frrlem12  8296  frrlem14  8298  wfrlem14OLD  8336  wfrlem16OLD  8338  mapsnd  8900  findcard2d  9180  ac6sfi  9292  iunfi  9355  elirrv  9610  kmlem2  10166  fin1a2lem10  10423  hsmexlem4  10443  iunfo  10553  modfsummodslem1  15808  lcmfunsnlem2lem1  16657  coprmprod  16680  coprmproddvdslem  16681  c0snmgmhm  20422  lbsextlem4  21122  frlmlbs  21757  coe1fzgsumdlem  22241  evl1gsumdlem  22294  maducoeval2  22578  dishaus  23320  dis2ndc  23398  dislly  23435  dissnlocfin  23467  comppfsc  23470  txdis  23570  txdis1cn  23573  txkgen  23590  isufil2  23846  alexsubALTlem4  23988  tmdgsum  24033  dscopn  24512  ovolfiniun  25454  volfiniun  25500  jensen  26951  uvtx01vtx  29376  cplgr1vlem  29408  unidifsnel  32516  gsumpart  33051  extdg1id  33707  irngss  33728  esum2dlem  34123  bnj1498  35092  funen1cnv  35119  wevgblacfn  35131  cvmlift2lem1  35324  funpartlem  35960  topdifinffinlem  37365  fvineqsneq  37430  pibt2  37435  finixpnum  37629  mbfresfi  37690  pclfinN  39919  sn-iotalem  42272  mzpcompact2lem  42774  dvmptfprod  45974  fourierdlem48  46183  sge0sup  46420  funressnvmo  47074  dfclnbgr6  47869  dfsclnbgr6  47871  termcarweu  49413  diag1f1o  49419  diag2f1o  49422