Theorem vsnid 4403

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

Syntax hints:   ∈ wcel 2156  {csn 4370

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-v 3393  df-sn 4371

This theorem is referenced by:  exsnrex  4414  rext  5106  unipw  5108  xpdifid  5773  opabiota  6478  fnressn  6645  fressnfv  6647  snnex  7192  snnexOLD  7193  wfrlem14  7660  wfrlem16  7662  findcard2d  8437  ac6sfi  8439  iunfi  8489  elirrv  8736  kmlem2  9254  fin1a2lem10  9512  hsmexlem4  9532  iunfo  9642  fsumsplitsnunOLD  14705  modfsummodslem1  14742  lcmfunsnlem2lem1  15566  coprmprod  15589  coprmproddvdslem  15590  lbsextlem4  19366  coe1fzgsumdlem  19875  evl1gsumdlem  19924  frlmlbs  20343  maducoeval2  20654  dishaus  21397  dis2ndc  21474  dislly  21511  dissnlocfin  21543  comppfsc  21546  txdis  21646  txdis1cn  21649  txkgen  21666  isufil2  21922  alexsubALTlem4  22064  tmdgsum  22109  dscopn  22588  ovolfiniun  23481  volfiniun  23527  jensen  24928  uvtx01vtx  26517  uvtxa01vtx0OLD  26519  cplgr1vlem  26552  esum2dlem  30478  bnj1498  31450  cvmlift2lem1  31605  funpartlem  32368  topdifinffinlem  33509  finixpnum  33705  mbfresfi  33766  pclfinN  35678  mzpcompact2lem  37813  fourierdlem48  40847  sge0sup  41084  funressnvmo  41661  c0snmgmhm  42479