Theorem vsnid 4663

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

Syntax hints:   ∈ wcel 2108  {csn 4626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-sn 4627

This theorem is referenced by:  exsnrex  4680  rext  5453  unipw  5455  xpdifid  6188  opabiota  6991  fnressn  7178  fressnfv  7180  snnex  7778  frrlem12  8322  frrlem14  8324  wfrlem14OLD  8362  wfrlem16OLD  8364  mapsnd  8926  findcard2d  9206  ac6sfi  9320  iunfi  9383  elirrv  9636  kmlem2  10192  fin1a2lem10  10449  hsmexlem4  10469  iunfo  10579  modfsummodslem1  15828  lcmfunsnlem2lem1  16675  coprmprod  16698  coprmproddvdslem  16699  c0snmgmhm  20462  lbsextlem4  21163  frlmlbs  21817  coe1fzgsumdlem  22307  evl1gsumdlem  22360  maducoeval2  22646  dishaus  23390  dis2ndc  23468  dislly  23505  dissnlocfin  23537  comppfsc  23540  txdis  23640  txdis1cn  23643  txkgen  23660  isufil2  23916  alexsubALTlem4  24058  tmdgsum  24103  dscopn  24586  ovolfiniun  25536  volfiniun  25582  jensen  27032  uvtx01vtx  29414  cplgr1vlem  29446  unidifsnel  32553  gsumpart  33060  extdg1id  33716  irngss  33737  esum2dlem  34093  bnj1498  35075  funen1cnv  35102  wevgblacfn  35114  cvmlift2lem1  35307  funpartlem  35943  topdifinffinlem  37348  fvineqsneq  37413  pibt2  37418  finixpnum  37612  mbfresfi  37673  pclfinN  39902  sn-iotalem  42260  mzpcompact2lem  42762  dvmptfprod  45960  fourierdlem48  46169  sge0sup  46406  funressnvmo  47057  dfclnbgr6  47842  dfsclnbgr6  47844