Theorem vsnid 4562

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

Syntax hints:   ∈ wcel 2111  {csn 4525

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-sn 4526

This theorem is referenced by:  exsnrex  4578  rext  5306  unipw  5308  xpdifid  5992  opabiota  6721  fnressn  6897  fressnfv  6899  snnex  7460  wfrlem14  7951  wfrlem16  7953  mapsnd  8433  findcard2d  8744  ac6sfi  8746  iunfi  8796  elirrv  9044  kmlem2  9562  fin1a2lem10  9820  hsmexlem4  9840  iunfo  9950  modfsummodslem1  15139  lcmfunsnlem2lem1  15972  coprmprod  15995  coprmproddvdslem  15996  lbsextlem4  19926  frlmlbs  20486  coe1fzgsumdlem  20930  evl1gsumdlem  20980  maducoeval2  21245  dishaus  21987  dis2ndc  22065  dislly  22102  dissnlocfin  22134  comppfsc  22137  txdis  22237  txdis1cn  22240  txkgen  22257  isufil2  22513  alexsubALTlem4  22655  tmdgsum  22700  dscopn  23180  ovolfiniun  24105  volfiniun  24151  jensen  25574  uvtx01vtx  27187  cplgr1vlem  27219  unidifsnel  30307  gsumpart  30740  extdg1id  31141  esum2dlem  31461  bnj1498  32443  funen1cnv  32467  cvmlift2lem1  32662  frrlem12  33247  frrlem14  33249  funpartlem  33516  topdifinffinlem  34764  fvineqsneq  34829  pibt2  34834  finixpnum  35042  mbfresfi  35103  pclfinN  37196  mzpcompact2lem  39692  fourierdlem48  42796  sge0sup  43030  funressnvmo  43637  c0snmgmhm  44538