Theorem vsnid 4619

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

Syntax hints:   ∈ wcel 2114  {csn 4579

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-v 3441  df-sn 4580

This theorem is referenced by:  exsnrex  4636  rext  5395  unipw  5397  xpdifid  6125  opabiota  6915  fnressn  7103  fressnfv  7105  snnex  7703  frrlem12  8239  frrlem14  8241  mapsnd  8826  findcard2d  9093  ac6sfi  9186  iunfi  9245  elirrvOLD  9505  kmlem2  10064  fin1a2lem10  10321  hsmexlem4  10341  iunfo  10451  modfsummodslem1  15717  lcmfunsnlem2lem1  16567  coprmprod  16590  coprmproddvdslem  16591  c0snmgmhm  20400  lbsextlem4  21118  frlmlbs  21754  coe1fzgsumdlem  22249  evl1gsumdlem  22302  maducoeval2  22586  dishaus  23328  dis2ndc  23406  dislly  23443  dissnlocfin  23475  comppfsc  23478  txdis  23578  txdis1cn  23581  txkgen  23598  isufil2  23854  alexsubALTlem4  23996  tmdgsum  24041  dscopn  24519  ovolfiniun  25460  volfiniun  25506  jensen  26957  uvtx01vtx  29451  cplgr1vlem  29483  unidifsnel  32590  gsumpart  33125  vieta  33715  extdg1id  33802  irngss  33823  esum2dlem  34228  bnj1498  35196  funen1cnv  35223  fineqvnttrclselem2  35257  wevgblacfn  35282  cvmlift2lem1  35475  funpartlem  36115  topdifinffinlem  37521  fvineqsneq  37586  pibt2  37591  finixpnum  37775  mbfresfi  37836  pclfinN  40195  sn-iotalem  42515  mzpcompact2lem  43030  dvmptfprod  46226  fourierdlem48  46435  sge0sup  46672  funressnvmo  47328  dfclnbgr6  48139  dfsclnbgr6  48141  termco  49763  termcarweu  49810  diag1f1o  49816  diag2f1o  49819