Theorem vsnid 4615

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

Syntax hints:   ∈ wcel 2109  {csn 4577

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-sn 4578

This theorem is referenced by:  exsnrex  4632  rext  5391  unipw  5393  xpdifid  6117  opabiota  6905  fnressn  7092  fressnfv  7094  snnex  7694  frrlem12  8230  frrlem14  8232  mapsnd  8813  findcard2d  9080  ac6sfi  9173  iunfi  9233  elirrvOLD  9490  kmlem2  10046  fin1a2lem10  10303  hsmexlem4  10323  iunfo  10433  modfsummodslem1  15699  lcmfunsnlem2lem1  16549  coprmprod  16572  coprmproddvdslem  16573  c0snmgmhm  20347  lbsextlem4  21068  frlmlbs  21704  coe1fzgsumdlem  22188  evl1gsumdlem  22241  maducoeval2  22525  dishaus  23267  dis2ndc  23345  dislly  23382  dissnlocfin  23414  comppfsc  23417  txdis  23517  txdis1cn  23520  txkgen  23537  isufil2  23793  alexsubALTlem4  23935  tmdgsum  23980  dscopn  24459  ovolfiniun  25400  volfiniun  25446  jensen  26897  uvtx01vtx  29346  cplgr1vlem  29378  unidifsnel  32484  gsumpart  33019  extdg1id  33649  irngss  33670  esum2dlem  34075  bnj1498  35044  funen1cnv  35071  fineqvnttrclselem2  35091  wevgblacfn  35102  cvmlift2lem1  35295  funpartlem  35936  topdifinffinlem  37341  fvineqsneq  37406  pibt2  37411  finixpnum  37605  mbfresfi  37666  pclfinN  39899  sn-iotalem  42214  mzpcompact2lem  42744  dvmptfprod  45946  fourierdlem48  46155  sge0sup  46392  funressnvmo  47049  dfclnbgr6  47860  dfsclnbgr6  47862  termco  49486  termcarweu  49533  diag1f1o  49539  diag2f1o  49542