Theorem vsnid 4621

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

Syntax hints:   ∈ wcel 2114  {csn 4581

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3443  df-sn 4582

This theorem is referenced by:  exsnrex  4638  rext  5397  unipw  5399  xpdifid  6127  opabiota  6917  fnressn  7105  fressnfv  7107  snnex  7705  frrlem12  8241  frrlem14  8243  mapsnd  8828  findcard2d  9095  ac6sfi  9188  iunfi  9247  elirrvOLD  9507  kmlem2  10066  fin1a2lem10  10323  hsmexlem4  10343  iunfo  10453  modfsummodslem1  15719  lcmfunsnlem2lem1  16569  coprmprod  16592  coprmproddvdslem  16593  c0snmgmhm  20402  lbsextlem4  21120  frlmlbs  21756  coe1fzgsumdlem  22251  evl1gsumdlem  22304  maducoeval2  22588  dishaus  23330  dis2ndc  23408  dislly  23445  dissnlocfin  23477  comppfsc  23480  txdis  23580  txdis1cn  23583  txkgen  23600  isufil2  23856  alexsubALTlem4  23998  tmdgsum  24043  dscopn  24521  ovolfiniun  25462  volfiniun  25508  jensen  26959  uvtx01vtx  29474  cplgr1vlem  29506  unidifsnel  32613  gsumpart  33148  vieta  33738  extdg1id  33825  irngss  33846  esum2dlem  34251  bnj1498  35219  funen1cnv  35246  fineqvnttrclselem2  35280  wevgblacfn  35305  cvmlift2lem1  35498  funpartlem  36138  exeltr  36667  topdifinffinlem  37554  fvineqsneq  37619  pibt2  37624  finixpnum  37808  mbfresfi  37869  pclfinN  40228  sn-iotalem  42545  mzpcompact2lem  43060  dvmptfprod  46256  fourierdlem48  46465  sge0sup  46702  funressnvmo  47358  dfclnbgr6  48169  dfsclnbgr6  48171  termco  49793  termcarweu  49840  diag1f1o  49846  diag2f1o  49849