Theorem vsnid 4185

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

Assertion

Ref	Expression
vsnid	⊢ 𝑥 ∈ {𝑥}

Proof of Theorem vsnid

Step	Hyp	Ref	Expression
1		vex 3194	. 2 ⊢ 𝑥 ∈ V
2	1	snid 4184	1 ⊢ 𝑥 ∈ {𝑥}

Syntax hints:   ∈ wcel 1992  {csn 4153

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-v 3193  df-sn 4154

This theorem is referenced by:  exsnrex  4197  rext  4882  unipw  4884  xpdifid  5525  opabiota  6219  fnressn  6380  fressnfv  6382  snnex  6918  wfrlem14  7374  wfrlem16  7376  findcard2d  8147  ac6sfi  8149  iunfi  8199  elirrv  8449  kmlem2  8918  fin1a2lem10  9176  hsmexlem4  9196  iunfo  9306  fsumsplitsnun  14409  fsumcom2OLD  14429  modfsummodslem1  14446  fprodcom2OLD  14635  lcmfunsnlem2lem1  15270  coprmprod  15294  coprmproddvdslem  15295  lbsextlem4  19075  coe1fzgsumdlem  19585  evl1gsumdlem  19634  frlmlbs  20050  maducoeval2  20360  dishaus  21091  dis2ndc  21168  dislly  21205  dissnlocfin  21237  comppfsc  21240  txdis  21340  txdis1cn  21343  txkgen  21360  isufil2  21617  alexsubALTlem4  21759  tmdgsum  21804  dscopn  22283  ovolfiniun  23171  volfiniun  23217  jensen  24610  uvtxa01vtx0  26178  cplgr1vlem  26206  frgrncvvdeqlem3  27023  frgrncvvdeqlem4  27024  frgrwopreg1  27039  frgrwopreg2  27040  esum2dlem  29927  bnj1498  30829  cvmlift2lem1  30984  funpartlem  31683  topdifinffinlem  32819  finixpnum  33012  mbfresfi  33074  pclfinN  34652  mzpcompact2lem  36780  fourierdlem48  39665  sge0sup  39902  c0snmgmhm  41175