Theorem vsnid 4628

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

Syntax hints:   ∈ wcel 2106  {csn 4591

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-sn 4592

This theorem is referenced by:  exsnrex  4646  rext  5410  unipw  5412  xpdifid  6125  opabiota  6929  fnressn  7109  fressnfv  7111  snnex  7697  frrlem12  8233  frrlem14  8235  wfrlem14OLD  8273  wfrlem16OLD  8275  mapsnd  8831  findcard2d  9117  ac6sfi  9238  iunfi  9291  elirrv  9541  kmlem2  10096  fin1a2lem10  10354  hsmexlem4  10374  iunfo  10484  modfsummodslem1  15688  lcmfunsnlem2lem1  16525  coprmprod  16548  coprmproddvdslem  16549  lbsextlem4  20681  frlmlbs  21240  coe1fzgsumdlem  21709  evl1gsumdlem  21759  maducoeval2  22026  dishaus  22770  dis2ndc  22848  dislly  22885  dissnlocfin  22917  comppfsc  22920  txdis  23020  txdis1cn  23023  txkgen  23040  isufil2  23296  alexsubALTlem4  23438  tmdgsum  23483  dscopn  23966  ovolfiniun  24902  volfiniun  24948  jensen  26375  uvtx01vtx  28408  cplgr1vlem  28440  unidifsnel  31526  gsumpart  31967  extdg1id  32439  irngss  32448  esum2dlem  32780  bnj1498  33762  funen1cnv  33781  cvmlift2lem1  33983  funpartlem  34603  topdifinffinlem  35891  fvineqsneq  35956  pibt2  35961  finixpnum  36136  mbfresfi  36197  pclfinN  38436  sn-iotalem  40714  mzpcompact2lem  41132  fourierdlem48  44515  sge0sup  44752  funressnvmo  45399  c0snmgmhm  46332