Theorem vsnid 4670

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

Syntax hints:   ∈ wcel 2099  {csn 4633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-v 3464  df-sn 4634

This theorem is referenced by:  exsnrex  4689  rext  5454  unipw  5456  xpdifid  6179  opabiota  6985  fnressn  7172  fressnfv  7174  snnex  7766  frrlem12  8312  frrlem14  8314  wfrlem14OLD  8352  wfrlem16OLD  8354  mapsnd  8915  findcard2d  9204  ac6sfi  9321  iunfi  9385  elirrv  9639  kmlem2  10194  fin1a2lem10  10452  hsmexlem4  10472  iunfo  10582  modfsummodslem1  15796  lcmfunsnlem2lem1  16639  coprmprod  16662  coprmproddvdslem  16663  c0snmgmhm  20444  lbsextlem4  21142  frlmlbs  21795  coe1fzgsumdlem  22294  evl1gsumdlem  22347  maducoeval2  22633  dishaus  23377  dis2ndc  23455  dislly  23492  dissnlocfin  23524  comppfsc  23527  txdis  23627  txdis1cn  23630  txkgen  23647  isufil2  23903  alexsubALTlem4  24045  tmdgsum  24090  dscopn  24573  ovolfiniun  25521  volfiniun  25567  jensen  27017  uvtx01vtx  29333  cplgr1vlem  29365  unidifsnel  32461  gsumpart  32923  extdg1id  33552  irngss  33563  esum2dlem  33925  bnj1498  34906  funen1cnv  34925  wevgblacfn  34936  cvmlift2lem1  35130  funpartlem  35766  topdifinffinlem  37054  fvineqsneq  37119  pibt2  37124  finixpnum  37306  mbfresfi  37367  pclfinN  39599  sn-iotalem  41943  mzpcompact2lem  42408  fourierdlem48  45775  sge0sup  46012  funressnvmo  46660  dfclnbgr6  47423  dfsclnbgr6  47425