Theorem vsnid 4608

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

Syntax hints:   ∈ wcel 2114  {csn 4568

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-sn 4569

This theorem is referenced by:  exsnrex  4625  rext  5397  unipw  5399  xpdifid  6128  opabiota  6918  fnressn  7107  fressnfv  7109  snnex  7707  frrlem12  8242  frrlem14  8244  mapsnd  8829  findcard2d  9096  ac6sfi  9189  iunfi  9248  elirrvOLD  9508  kmlem2  10069  fin1a2lem10  10326  hsmexlem4  10346  iunfo  10456  modfsummodslem1  15750  lcmfunsnlem2lem1  16602  coprmprod  16625  coprmproddvdslem  16626  c0snmgmhm  20437  lbsextlem4  21155  frlmlbs  21791  coe1fzgsumdlem  22282  evl1gsumdlem  22335  maducoeval2  22619  dishaus  23361  dis2ndc  23439  dislly  23476  dissnlocfin  23508  comppfsc  23511  txdis  23611  txdis1cn  23614  txkgen  23631  isufil2  23887  alexsubALTlem4  24029  tmdgsum  24074  dscopn  24552  ovolfiniun  25482  volfiniun  25528  jensen  26970  uvtx01vtx  29484  cplgr1vlem  29516  unidifsnel  32624  gsumpart  33143  vieta  33743  extdg1id  33830  irngss  33851  esum2dlem  34256  bnj1498  35223  funen1cnv  35251  fineqvnttrclselem2  35286  wevgblacfn  35311  cvmlift2lem1  35504  funpartlem  36144  ttcid  36694  topdifinffinlem  37683  fvineqsneq  37748  pibt2  37753  finixpnum  37946  mbfresfi  38007  pclfinN  40366  sn-iotalem  42682  mzpcompact2lem  43203  dvmptfprod  46397  fourierdlem48  46606  sge0sup  46843  funressnvmo  47511  dfclnbgr6  48350  dfsclnbgr6  48352  termco  49974  termcarweu  50021  diag1f1o  50027  diag2f1o  50030