Theorem vsnid 4627

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

Syntax hints:   ∈ wcel 2109  {csn 4589

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 3449  df-sn 4590

This theorem is referenced by:  exsnrex  4644  rext  5408  unipw  5410  xpdifid  6141  opabiota  6943  fnressn  7130  fressnfv  7132  snnex  7734  frrlem12  8276  frrlem14  8278  mapsnd  8859  findcard2d  9130  ac6sfi  9231  iunfi  9294  elirrv  9549  kmlem2  10105  fin1a2lem10  10362  hsmexlem4  10382  iunfo  10492  modfsummodslem1  15758  lcmfunsnlem2lem1  16608  coprmprod  16631  coprmproddvdslem  16632  c0snmgmhm  20371  lbsextlem4  21071  frlmlbs  21706  coe1fzgsumdlem  22190  evl1gsumdlem  22243  maducoeval2  22527  dishaus  23269  dis2ndc  23347  dislly  23384  dissnlocfin  23416  comppfsc  23419  txdis  23519  txdis1cn  23522  txkgen  23539  isufil2  23795  alexsubALTlem4  23937  tmdgsum  23982  dscopn  24461  ovolfiniun  25402  volfiniun  25448  jensen  26899  uvtx01vtx  29324  cplgr1vlem  29356  unidifsnel  32464  gsumpart  32997  extdg1id  33661  irngss  33682  esum2dlem  34082  bnj1498  35051  funen1cnv  35078  wevgblacfn  35096  cvmlift2lem1  35289  funpartlem  35930  topdifinffinlem  37335  fvineqsneq  37400  pibt2  37405  finixpnum  37599  mbfresfi  37660  pclfinN  39894  sn-iotalem  42209  mzpcompact2lem  42739  dvmptfprod  45943  fourierdlem48  46152  sge0sup  46389  funressnvmo  47046  dfclnbgr6  47856  dfsclnbgr6  47858  termco  49470  termcarweu  49517  diag1f1o  49523  diag2f1o  49526