Theorem vsnid 4598

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

Syntax hints:   ∈ wcel 2121  {csn 4558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-v 3435  df-sn 4559

This theorem is referenced by:  exsnrex  4615  rext  5390  unipw  5392  xpdifid  6123  opabiota  6913  fnressn  7105  fressnfv  7107  snnex  7705  frrlem12  8241  frrlem14  8243  mapsnd  8828  findcard2d  9095  ac6sfi  9188  iunfi  9247  elirrvOLDOLD  9508  kmlem2  10069  fin1a2lem10  10326  hsmexlem4  10346  iunfo  10456  modfsummodslem1  15750  lcmfunsnlem2lem1  16602  coprmprod  16625  coprmproddvdslem  16626  c0snmgmhm  20437  lbsextlem4  21158  frlmlbs  21776  coe1fzgsumdlem  22293  evl1gsumdlem  22346  maducoeval2  22627  dishaus  23369  dis2ndc  23447  dislly  23484  dissnlocfin  23516  comppfsc  23519  txdis  23619  txdis1cn  23622  txkgen  23639  isufil2  23895  alexsubALTlem4  24037  tmdgsum  24082  dscopn  24560  ovolfiniun  25490  volfiniun  25536  jensen  26974  uvtx01vtx  29488  cplgr1vlem  29520  unidifsnel  32627  gsumpart  33148  dflring3  33592  mplidomlem  33723  vieta  33776  extdg1id  33862  irngss  33883  esum2dlem  34288  bnj1498  35258  funen1cnv  35284  fineqvnttrclselem2  35318  wevgblacfn  35352  cvmlift2lem1  35545  funpartlem  36185  ttcid  36735  topdifinffinlem  37724  fvineqsneq  37789  pibt2  37794  finixpnum  37987  mbfresfi  38048  pclfinN  40407  sn-iotalem  42723  mzpcompact2lem  43215  dvmptfprod  46402  fourierdlem48  46611  sge0sup  46848  funressnvmo  47522  dfclnbgr6  48361  dfsclnbgr6  48363  termco  49985  termcarweu  50032  diag1f1o  50038  diag2f1o  50041