Theorem vsnid 4603

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

Syntax hints:   ∈ wcel 2109  {csn 4566

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1544  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3432  df-sn 4567

This theorem is referenced by:  exsnrex  4621  rext  5366  unipw  5368  xpdifid  6068  opabiota  6845  fnressn  7024  fressnfv  7026  snnex  7599  frrlem12  8097  frrlem14  8099  wfrlem14OLD  8137  wfrlem16OLD  8139  mapsnd  8648  findcard2d  8914  ac6sfi  9019  iunfi  9068  elirrv  9316  kmlem2  9891  fin1a2lem10  10149  hsmexlem4  10169  iunfo  10279  modfsummodslem1  15485  lcmfunsnlem2lem1  16324  coprmprod  16347  coprmproddvdslem  16348  lbsextlem4  20404  frlmlbs  20985  coe1fzgsumdlem  21453  evl1gsumdlem  21503  maducoeval2  21770  dishaus  22514  dis2ndc  22592  dislly  22629  dissnlocfin  22661  comppfsc  22664  txdis  22764  txdis1cn  22767  txkgen  22784  isufil2  23040  alexsubALTlem4  23182  tmdgsum  23227  dscopn  23710  ovolfiniun  24646  volfiniun  24692  jensen  26119  uvtx01vtx  27745  cplgr1vlem  27777  unidifsnel  30862  gsumpart  31294  extdg1id  31717  esum2dlem  32039  bnj1498  33020  funen1cnv  33039  cvmlift2lem1  33243  funpartlem  34223  topdifinffinlem  35497  fvineqsneq  35562  pibt2  35567  finixpnum  35741  mbfresfi  35802  pclfinN  37893  sn-iotalem  40169  mzpcompact2lem  40553  fourierdlem48  43649  sge0sup  43883  funressnvmo  44490  c0snmgmhm  45424