Theorem vsnid 4667

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

Syntax hints:   ∈ wcel 2105  {csn 4630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-sn 4631

This theorem is referenced by:  exsnrex  4684  rext  5458  unipw  5460  xpdifid  6189  opabiota  6990  fnressn  7177  fressnfv  7179  snnex  7776  frrlem12  8320  frrlem14  8322  wfrlem14OLD  8360  wfrlem16OLD  8362  mapsnd  8924  findcard2d  9204  ac6sfi  9317  iunfi  9380  elirrv  9633  kmlem2  10189  fin1a2lem10  10446  hsmexlem4  10466  iunfo  10576  modfsummodslem1  15824  lcmfunsnlem2lem1  16671  coprmprod  16694  coprmproddvdslem  16695  c0snmgmhm  20478  lbsextlem4  21180  frlmlbs  21834  coe1fzgsumdlem  22322  evl1gsumdlem  22375  maducoeval2  22661  dishaus  23405  dis2ndc  23483  dislly  23520  dissnlocfin  23552  comppfsc  23555  txdis  23655  txdis1cn  23658  txkgen  23675  isufil2  23931  alexsubALTlem4  24073  tmdgsum  24118  dscopn  24601  ovolfiniun  25549  volfiniun  25595  jensen  27046  uvtx01vtx  29428  cplgr1vlem  29460  unidifsnel  32560  gsumpart  33042  extdg1id  33690  irngss  33701  esum2dlem  34072  bnj1498  35053  funen1cnv  35080  wevgblacfn  35092  cvmlift2lem1  35286  funpartlem  35923  topdifinffinlem  37329  fvineqsneq  37394  pibt2  37399  finixpnum  37591  mbfresfi  37652  pclfinN  39882  sn-iotalem  42238  mzpcompact2lem  42738  dvmptfprod  45900  fourierdlem48  46109  sge0sup  46346  funressnvmo  46994  dfclnbgr6  47779  dfsclnbgr6  47781