Theorem vsnid 4209

Description: A setvar variable is a member of its singleton (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)

Assertion

Ref	Expression
vsnid	|- x e. { x }

Proof of Theorem vsnid

Step	Hyp	Ref	Expression
1		vex 3203	. 2 |- x e. _V
2	1	snid 4208	1 |- x e. { x }

Syntax hints:   e. wcel 1990   {csn 4177

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-sn 4178

This theorem is referenced by:  exsnrex  4221  rext  4916  unipw  4918  xpdifid  5562  opabiota  6261  fnressn  6425  fressnfv  6427  snnex  6966  snnexOLD  6967  wfrlem14  7428  wfrlem16  7430  findcard2d  8202  ac6sfi  8204  iunfi  8254  elirrv  8504  kmlem2  8973  fin1a2lem10  9231  hsmexlem4  9251  iunfo  9361  fsumsplitsnunOLD  14486  fsumcom2OLD  14506  modfsummodslem1  14524  fprodcom2OLD  14715  lcmfunsnlem2lem1  15351  coprmprod  15375  coprmproddvdslem  15376  lbsextlem4  19161  coe1fzgsumdlem  19671  evl1gsumdlem  19720  frlmlbs  20136  maducoeval2  20446  dishaus  21186  dis2ndc  21263  dislly  21300  dissnlocfin  21332  comppfsc  21335  txdis  21435  txdis1cn  21438  txkgen  21455  isufil2  21712  alexsubALTlem4  21854  tmdgsum  21899  dscopn  22378  ovolfiniun  23269  volfiniun  23315  jensen  24715  uvtxa01vtx0  26297  cplgr1vlem  26325  esum2dlem  30154  bnj1498  31129  cvmlift2lem1  31284  funpartlem  32049  topdifinffinlem  33195  finixpnum  33394  mbfresfi  33456  pclfinN  35186  mzpcompact2lem  37314  fourierdlem48  40371  sge0sup  40608  c0snmgmhm  41914