Theorem vsnid 4666

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

Syntax hints:   ∈ wcel 2107  {csn 4629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-sn 4630

This theorem is referenced by:  exsnrex  4685  rext  5449  unipw  5451  xpdifid  6168  opabiota  6975  fnressn  7156  fressnfv  7158  snnex  7745  frrlem12  8282  frrlem14  8284  wfrlem14OLD  8322  wfrlem16OLD  8324  mapsnd  8880  findcard2d  9166  ac6sfi  9287  iunfi  9340  elirrv  9591  kmlem2  10146  fin1a2lem10  10404  hsmexlem4  10424  iunfo  10534  modfsummodslem1  15738  lcmfunsnlem2lem1  16575  coprmprod  16598  coprmproddvdslem  16599  lbsextlem4  20774  frlmlbs  21352  coe1fzgsumdlem  21825  evl1gsumdlem  21875  maducoeval2  22142  dishaus  22886  dis2ndc  22964  dislly  23001  dissnlocfin  23033  comppfsc  23036  txdis  23136  txdis1cn  23139  txkgen  23156  isufil2  23412  alexsubALTlem4  23554  tmdgsum  23599  dscopn  24082  ovolfiniun  25018  volfiniun  25064  jensen  26493  uvtx01vtx  28654  cplgr1vlem  28686  unidifsnel  31772  gsumpart  32207  extdg1id  32742  irngss  32751  esum2dlem  33090  bnj1498  34072  funen1cnv  34091  cvmlift2lem1  34293  funpartlem  34914  topdifinffinlem  36228  fvineqsneq  36293  pibt2  36298  finixpnum  36473  mbfresfi  36534  pclfinN  38771  sn-iotalem  41038  mzpcompact2lem  41489  fourierdlem48  44870  sge0sup  45107  funressnvmo  45755  c0snmgmhm  46713