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

This proof depends on syntax axioms:   ∈ wcel 2142  {csn 4588

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-sn 4589

This theorem is used by:  exsnrex  4645  rext  5428  unipw  5430  xpdifid  6164  xpdifcnvepel  6165  opabiota  6963  fnressn  7155  fressnfv  7157  snnex  7755  frrlem12  8292  frrlem14  8294  mapsnd  8882  findcard2d  9149  ac6sfi  9242  iunfi  9298  elirrvOLDOLD  9559  kmlem2  10142  fin1a2lem10  10399  hsmexlem4  10419  iunfo  10529  modfsummodslem1  15851  lcmfunsnlem2lem1  16702  coprmprod  16725  coprmproddvdslem  16726  c0snmgmhm  20551  lbsextlem4  21296  frlmlbs  21958  coe1fzgsumdlem  22474  evl1gsumdlem  22527  maducoeval2  22808  dishaus  23550  dis2ndc  23628  dislly  23665  dissnlocfin  23697  comppfsc  23700  txdis  23800  txdis1cn  23803  txkgen  23820  isufil2  24076  alexsubALTlem4  24218  tmdgsum  24263  dscopn  24741  ovolfiniun  25671  volfiniun  25717  jensen  27164  uvtx01vtx  29758  cplgr1vlem  29790  unidifsnel  32892  gsumpart  33392  dflring3  33796  mplidomlem  33926  vieta  33979  extdg1id  34065  irngss  34086  esum2dlem  34491  bnj1498  35458  funen1cnv  35486  fineqvnttrclselem2  35543  wevgblacfn  35603  cvmlift2lem1  35802  funpartlem  36442  ttcid  37031  topdifinffinlem  38021  fvineqsneq  38086  pibt2  38091  finixpnum  38284  mbfresfi  38345  pclfinN  40702  sn-iotalem  43020  mzpcompact2lem  43510  dvmptfprod  46687  fourierdlem48  46896  sge0sup  47133  funressnvmo  47810  dfclnbgr6  48649  dfsclnbgr6  48651  termco  50287  termcarweu  50334  diag1f1o  50340  diag2f1o  50343