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

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

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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-sn 4585

This theorem is used by:  exsnrex  4641  rext  5416  unipw  5418  xpdifid  6155  xpdifcnvepel  6156  opabiota  6956  fnressn  7151  fressnfv  7153  snnex  7756  frrlem12  8294  frrlem14  8296  mapsnd  8893  funen1cnv  9035  findcard2d  9161  ac6sfi  9254  iunfi  9310  elirrvOLDOLD  9571  kmlem2  10187  fin1a2lem10  10444  hsmexlem4  10464  iunfo  10580  modfsummodslem1  15912  lcmfunsnlem2lem1  16761  coprmprod  16784  coprmproddvdslem  16785  c0snmgmhm  20639  lbsextlem4  21386  frlmlbs  22050  coe1fzgsumdlem  22568  evl1gsumdlem  22621  maducoeval2  22902  dishaus  23647  dis2ndc  23726  dislly  23763  dissnlocfin  23795  comppfsc  23798  txdis  23898  txdis1cn  23901  txkgen  23918  isufil2  24174  alexsubALTlem4  24316  tmdgsum  24361  dscopn  24839  ovolfiniun  25769  volfiniun  25815  jensen  27265  uvtx01vtx  29897  cplgr1vlem  29929  unidifsnel  33050  gsumpart  33543  dflring3  33948  mplidomlem  34078  vieta  34131  extdg1id  34217  irngss  34238  esum2dlem  34643  bnj1498  35611  fineqvnttrclselem2  35709  wevgblacfn  35809  cvmlift2lem1  35982  funpartlem  36622  ttcid  37196  topdifinffinlem  38184  fvineqsneq  38249  pibt2  38254  finixpnum  38442  mbfresfi  38498  pclfinN  40871  sn-iotalem  43189  mzpcompact2lem  43694  dvmptfprod  46871  fourierdlem48  47080  sge0sup  47317  funressnvmo  48031  dfclnbgr6  48870  dfsclnbgr6  48872  termco  50505  termcarweu  50552  diag1f1o  50558  diag2f1o  50561