Theorem vsnid 4354

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

Syntax hints:   ∈ wcel 2139  {csn 4321

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-v 3342  df-sn 4322

This theorem is referenced by:  exsnrex  4365  rext  5065  unipw  5067  xpdifid  5720  opabiota  6423  fnressn  6588  fressnfv  6590  snnex  7131  snnexOLD  7132  wfrlem14  7597  wfrlem16  7599  findcard2d  8367  ac6sfi  8369  iunfi  8419  elirrv  8666  kmlem2  9165  fin1a2lem10  9423  hsmexlem4  9443  iunfo  9553  fsumsplitsnunOLD  14685  fsumcom2OLD  14705  modfsummodslem1  14723  fprodcom2OLD  14914  lcmfunsnlem2lem1  15553  coprmprod  15577  coprmproddvdslem  15578  lbsextlem4  19363  coe1fzgsumdlem  19873  evl1gsumdlem  19922  frlmlbs  20338  maducoeval2  20648  dishaus  21388  dis2ndc  21465  dislly  21502  dissnlocfin  21534  comppfsc  21537  txdis  21637  txdis1cn  21640  txkgen  21657  isufil2  21913  alexsubALTlem4  22055  tmdgsum  22100  dscopn  22579  ovolfiniun  23469  volfiniun  23515  jensen  24914  uvtx01vtx  26500  uvtxa01vtx0OLD  26502  cplgr1vlem  26535  esum2dlem  30463  bnj1498  31436  cvmlift2lem1  31591  funpartlem  32355  topdifinffinlem  33506  finixpnum  33707  mbfresfi  33769  pclfinN  35689  mzpcompact2lem  37816  fourierdlem48  40874  sge0sup  41111  c0snmgmhm  42424