Theorem vsnid 4627

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

This proof depends on syntax axioms:   ∈ wcel 2145  {csn 4587

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-sn 4588

This theorem is used by:  exsnrex  4644  rext  5427  unipw  5429  xpdifid  6164  xpdifcnvepel  6165  opabiota  6964  fnressn  7158  fressnfv  7160  snnex  7760  frrlem12  8299  frrlem14  8301  mapsnd  8896  funen1cnv  9038  findcard2d  9164  ac6sfi  9257  iunfi  9313  elirrvOLDOLD  9574  kmlem2  10157  fin1a2lem10  10414  hsmexlem4  10434  iunfo  10550  modfsummodslem1  15881  lcmfunsnlem2lem1  16732  coprmprod  16755  coprmproddvdslem  16756  c0snmgmhm  20604  lbsextlem4  21349  frlmlbs  22011  coe1fzgsumdlem  22529  evl1gsumdlem  22582  maducoeval2  22863  dishaus  23608  dis2ndc  23687  dislly  23724  dissnlocfin  23756  comppfsc  23759  txdis  23859  txdis1cn  23862  txkgen  23879  isufil2  24135  alexsubALTlem4  24277  tmdgsum  24322  dscopn  24800  ovolfiniun  25730  volfiniun  25776  jensen  27223  uvtx01vtx  29843  cplgr1vlem  29875  unidifsnel  32996  gsumpart  33490  dflring3  33894  mplidomlem  34024  vieta  34077  extdg1id  34163  irngss  34184  esum2dlem  34589  bnj1498  35557  fineqvnttrclselem2  35635  wevgblacfn  35695  cvmlift2lem1  35868  funpartlem  36508  ttcid  37098  topdifinffinlem  38088  fvineqsneq  38153  pibt2  38158  finixpnum  38346  mbfresfi  38402  pclfinN  40760  sn-iotalem  43078  mzpcompact2lem  43583  dvmptfprod  46760  fourierdlem48  46969  sge0sup  47206  funressnvmo  47920  dfclnbgr6  48759  dfsclnbgr6  48761  termco  50394  termcarweu  50441  diag1f1o  50447  diag2f1o  50450