Theorem vsnid 4685

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

Syntax hints:   ∈ wcel 2108  {csn 4648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-sn 4649

This theorem is referenced by:  exsnrex  4704  rext  5468  unipw  5470  xpdifid  6199  opabiota  7004  fnressn  7192  fressnfv  7194  snnex  7793  frrlem12  8338  frrlem14  8340  wfrlem14OLD  8378  wfrlem16OLD  8380  mapsnd  8944  findcard2d  9232  ac6sfi  9348  iunfi  9411  elirrv  9665  kmlem2  10221  fin1a2lem10  10478  hsmexlem4  10498  iunfo  10608  modfsummodslem1  15840  lcmfunsnlem2lem1  16685  coprmprod  16708  coprmproddvdslem  16709  c0snmgmhm  20488  lbsextlem4  21186  frlmlbs  21840  coe1fzgsumdlem  22328  evl1gsumdlem  22381  maducoeval2  22667  dishaus  23411  dis2ndc  23489  dislly  23526  dissnlocfin  23558  comppfsc  23561  txdis  23661  txdis1cn  23664  txkgen  23681  isufil2  23937  alexsubALTlem4  24079  tmdgsum  24124  dscopn  24607  ovolfiniun  25555  volfiniun  25601  jensen  27050  uvtx01vtx  29432  cplgr1vlem  29464  unidifsnel  32563  gsumpart  33038  extdg1id  33676  irngss  33687  esum2dlem  34056  bnj1498  35037  funen1cnv  35064  wevgblacfn  35076  cvmlift2lem1  35270  funpartlem  35906  topdifinffinlem  37313  fvineqsneq  37378  pibt2  37383  finixpnum  37565  mbfresfi  37626  pclfinN  39857  sn-iotalem  42214  mzpcompact2lem  42707  fourierdlem48  46075  sge0sup  46312  funressnvmo  46960  dfclnbgr6  47728  dfsclnbgr6  47730