Theorem vsnid 4623

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

Syntax hints:   ∈ wcel 2109  {csn 4585

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 3446  df-sn 4586

This theorem is referenced by:  exsnrex  4640  rext  5403  unipw  5405  xpdifid  6129  opabiota  6925  fnressn  7112  fressnfv  7114  snnex  7714  frrlem12  8253  frrlem14  8255  mapsnd  8836  findcard2d  9107  ac6sfi  9207  iunfi  9270  elirrv  9525  kmlem2  10081  fin1a2lem10  10338  hsmexlem4  10358  iunfo  10468  modfsummodslem1  15734  lcmfunsnlem2lem1  16584  coprmprod  16607  coprmproddvdslem  16608  c0snmgmhm  20382  lbsextlem4  21103  frlmlbs  21739  coe1fzgsumdlem  22223  evl1gsumdlem  22276  maducoeval2  22560  dishaus  23302  dis2ndc  23380  dislly  23417  dissnlocfin  23449  comppfsc  23452  txdis  23552  txdis1cn  23555  txkgen  23572  isufil2  23828  alexsubALTlem4  23970  tmdgsum  24015  dscopn  24494  ovolfiniun  25435  volfiniun  25481  jensen  26932  uvtx01vtx  29377  cplgr1vlem  29409  unidifsnel  32514  gsumpart  33040  extdg1id  33654  irngss  33675  esum2dlem  34075  bnj1498  35044  funen1cnv  35071  wevgblacfn  35089  cvmlift2lem1  35282  funpartlem  35923  topdifinffinlem  37328  fvineqsneq  37393  pibt2  37398  finixpnum  37592  mbfresfi  37653  pclfinN  39887  sn-iotalem  42202  mzpcompact2lem  42732  dvmptfprod  45936  fourierdlem48  46145  sge0sup  46382  funressnvmo  47039  dfclnbgr6  47849  dfsclnbgr6  47851  termco  49463  termcarweu  49510  diag1f1o  49516  diag2f1o  49519