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

This proof depends on syntax axioms:   ∈ wcel 2144  {csn 4583

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-sn 4584

This theorem is used by:  exsnrex  4640  rext  5415  unipw  5417  xpdifid  6158  xpdifcnvepel  6159  opabiota  6967  fnressn  7162  fressnfv  7164  snnex  7772  frrlem12  8315  frrlem14  8317  mapsnd  8914  funen1cnv  9056  findcard2d  9182  ac6sfi  9275  iunfi  9332  elirrvOLDOLD  9593  kmlem2  10230  fin1a2lem10  10487  hsmexlem4  10507  iunfo  10623  modfsummodslem1  15959  lcmfunsnlem2lem1  16813  coprmprod  16836  coprmproddvdslem  16837  c0snmgmhm  20692  lbsextlem4  21439  frlmlbs  22103  coe1fzgsumdlem  22621  evl1gsumdlem  22674  maducoeval2  22955  dishaus  23700  dis2ndc  23779  dislly  23816  dissnlocfin  23848  comppfsc  23851  txdis  23951  txdis1cn  23954  txkgen  23971  isufil2  24227  alexsubALTlem4  24369  tmdgsum  24414  dscopn  24892  ovolfiniun  25822  volfiniun  25868  jensen  27316  uvtx01vtx  29978  cplgr1vlem  30010  unidifsnel  33131  gsumpart  33624  dflring3  34029  mplidomlem  34159  vieta  34212  extdg1id  34298  irngss  34319  esum2dlem  34724  bnj1498  35691  fineqvnttrclselem2  35790  wevgblacfn  35890  cvmlift2lem1  36067  funpartlem  36706  ttcid  37280  topdifinffinlem  38271  fvineqsneq  38336  pibt2  38341  finixpnum  38529  mbfresfi  38585  pclfinN  40958  sn-iotalem  43276  mzpcompact2lem  43762  dvmptfprod  46955  fourierdlem48  47164  sge0sup  47401  funressnvmo  48115  dfclnbgr6  48954  dfsclnbgr6  48956  termco  50589  termcarweu  50636  diag1f1o  50642  diag2f1o  50645