Theorem vsnid 4613

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

Syntax hints:   ∈ wcel 2111  {csn 4573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-sn 4574

This theorem is referenced by:  exsnrex  4630  rext  5387  unipw  5389  xpdifid  6115  opabiota  6904  fnressn  7091  fressnfv  7093  snnex  7691  frrlem12  8227  frrlem14  8229  mapsnd  8810  findcard2d  9076  ac6sfi  9168  iunfi  9227  elirrvOLD  9484  kmlem2  10043  fin1a2lem10  10300  hsmexlem4  10320  iunfo  10430  modfsummodslem1  15699  lcmfunsnlem2lem1  16549  coprmprod  16572  coprmproddvdslem  16573  c0snmgmhm  20380  lbsextlem4  21098  frlmlbs  21734  coe1fzgsumdlem  22218  evl1gsumdlem  22271  maducoeval2  22555  dishaus  23297  dis2ndc  23375  dislly  23412  dissnlocfin  23444  comppfsc  23447  txdis  23547  txdis1cn  23550  txkgen  23567  isufil2  23823  alexsubALTlem4  23965  tmdgsum  24010  dscopn  24488  ovolfiniun  25429  volfiniun  25475  jensen  26926  uvtx01vtx  29375  cplgr1vlem  29407  unidifsnel  32515  gsumpart  33037  extdg1id  33679  irngss  33700  esum2dlem  34105  bnj1498  35073  funen1cnv  35100  fineqvnttrclselem2  35142  wevgblacfn  35153  cvmlift2lem1  35346  funpartlem  35986  topdifinffinlem  37391  fvineqsneq  37456  pibt2  37461  finixpnum  37644  mbfresfi  37705  pclfinN  39998  sn-iotalem  42313  mzpcompact2lem  42843  dvmptfprod  46042  fourierdlem48  46251  sge0sup  46488  funressnvmo  47144  dfclnbgr6  47955  dfsclnbgr6  47957  termco  49581  termcarweu  49628  diag1f1o  49634  diag2f1o  49637