Theorem vsnid 4624

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 4623	1 ⊢ 𝑥 ∈ {𝑥}

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-sn 4589

This theorem is used by:  exsnrex  4641  rext  5420  unipw  5422  xpdifid  6170  xpdifcnvepel  6171  opabiota  6987  fnressn  7183  fressnfv  7185  snnex  7793  frrlem12  8340  frrlem14  8342  mapsnd  8939  funen1cnv  9081  findcard2d  9207  ac6sfi  9300  iunfi  9357  elirrvOLDOLD  9617  kmlem2  10254  fin1a2lem10  10511  hsmexlem4  10531  iunfo  10647  modfsummodslem1  15985  lcmfunsnlem2lem1  16839  coprmprod  16862  coprmproddvdslem  16863  c0snmgmhm  20719  lbsextlem4  21466  frlmlbs  22130  coe1fzgsumdlem  22648  evl1gsumdlem  22701  maducoeval2  22982  dishaus  23727  dis2ndc  23806  dislly  23843  dissnlocfin  23875  comppfsc  23878  txdis  23978  txdis1cn  23981  txkgen  23998  isufil2  24254  alexsubALTlem4  24396  tmdgsum  24441  dscopn  24919  ovolfiniun  25849  volfiniun  25895  jensen  27343  uvtx01vtx  30005  cplgr1vlem  30037  unidifsnel  33200  gsumpart  33691  dflring3  34096  mplidomlem  34226  vieta  34279  extdg1id  34365  irngss  34386  esum2dlem  34791  bnj1498  35758  fineqvnttrclselem2  35889  wevgblacfn  36038  cvmlift2lem1  36233  elpssmo  36635  funpartlem  36883  ttcid  37457  topdifinffinlem  38461  fvineqsneq  38526  pibt2  38531  finixpnum  38719  mbfresfi  38775  pclfinN  41148  sn-iotalem  43466  mzpcompact2lem  43953  dvmptfprod  47158  fourierdlem48  47367  sge0sup  47604  funressnvmo  48318  dfclnbgr6  49157  dfsclnbgr6  49159  termco  50819  termcarweu  50866  diag1f1o  50872  diag2f1o  50878