Theorem vsnid 4624

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

Syntax hints:   ∈ wcel 2144  {csn 4584

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1565  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-v 3458  df-sn 4585

This theorem is referenced by:  exsnrex  4641  rext  5417  unipw  5419  xpdifid  6155  xpdifcnvepel  6156  opabiota  6951  fnressn  7143  fressnfv  7145  snnex  7743  frrlem12  8280  frrlem14  8282  mapsnd  8870  findcard2d  9137  ac6sfi  9230  iunfi  9288  elirrvOLDOLD  9549  kmlem2  10110  fin1a2lem10  10368  hsmexlem4  10388  iunfo  10498  modfsummodslem1  15822  lcmfunsnlem2lem1  16674  coprmprod  16697  coprmproddvdslem  16698  c0snmgmhm  20513  lbsextlem4  21233  frlmlbs  21851  coe1fzgsumdlem  22368  evl1gsumdlem  22421  maducoeval2  22702  dishaus  23444  dis2ndc  23522  dislly  23559  dissnlocfin  23591  comppfsc  23594  txdis  23694  txdis1cn  23697  txkgen  23714  isufil2  23970  alexsubALTlem4  24112  tmdgsum  24157  dscopn  24635  ovolfiniun  25565  volfiniun  25611  jensen  27055  uvtx01vtx  29600  cplgr1vlem  29632  unidifsnel  32736  gsumpart  33245  dflring3  33695  mplidomlem  33826  vieta  33879  extdg1id  33965  irngss  33986  esum2dlem  34391  bnj1498  35358  funen1cnv  35384  fineqvnttrclselem2  35422  wevgblacfn  35458  cvmlift2lem1  35657  funpartlem  36297  ttcid  36857  topdifinffinlem  37846  fvineqsneq  37911  pibt2  37916  finixpnum  38109  mbfresfi  38170  pclfinN  40529  sn-iotalem  42845  mzpcompact2lem  43337  dvmptfprod  46524  fourierdlem48  46733  sge0sup  46970  funressnvmo  47644  dfclnbgr6  48483  dfsclnbgr6  48485  termco  50107  termcarweu  50154  diag1f1o  50160  diag2f1o  50163