Theorem vsnid 4607

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

Syntax hints:   ∈ wcel 2114  {csn 4567

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-sn 4568

This theorem is referenced by:  exsnrex  4624  rext  5400  unipw  5402  xpdifid  6132  opabiota  6922  fnressn  7112  fressnfv  7114  snnex  7712  frrlem12  8247  frrlem14  8249  mapsnd  8834  findcard2d  9101  ac6sfi  9194  iunfi  9253  elirrvOLD  9513  kmlem2  10074  fin1a2lem10  10331  hsmexlem4  10351  iunfo  10461  modfsummodslem1  15755  lcmfunsnlem2lem1  16607  coprmprod  16630  coprmproddvdslem  16631  c0snmgmhm  20442  lbsextlem4  21159  frlmlbs  21777  coe1fzgsumdlem  22268  evl1gsumdlem  22321  maducoeval2  22605  dishaus  23347  dis2ndc  23425  dislly  23462  dissnlocfin  23494  comppfsc  23497  txdis  23597  txdis1cn  23600  txkgen  23617  isufil2  23873  alexsubALTlem4  24015  tmdgsum  24060  dscopn  24538  ovolfiniun  25468  volfiniun  25514  jensen  26952  uvtx01vtx  29466  cplgr1vlem  29498  unidifsnel  32605  gsumpart  33124  vieta  33724  extdg1id  33810  irngss  33831  esum2dlem  34236  bnj1498  35203  funen1cnv  35231  fineqvnttrclselem2  35266  wevgblacfn  35291  cvmlift2lem1  35484  funpartlem  36124  ttcid  36674  topdifinffinlem  37663  fvineqsneq  37728  pibt2  37733  finixpnum  37926  mbfresfi  37987  pclfinN  40346  sn-iotalem  42662  mzpcompact2lem  43183  dvmptfprod  46373  fourierdlem48  46582  sge0sup  46819  funressnvmo  47493  dfclnbgr6  48332  dfsclnbgr6  48334  termco  49956  termcarweu  50003  diag1f1o  50009  diag2f1o  50012