Theorem vsnid 4630

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

Syntax hints:   ∈ wcel 2109  {csn 4592

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-sn 4593

This theorem is referenced by:  exsnrex  4647  rext  5411  unipw  5413  xpdifid  6144  opabiota  6946  fnressn  7133  fressnfv  7135  snnex  7737  frrlem12  8279  frrlem14  8281  mapsnd  8862  findcard2d  9136  ac6sfi  9238  iunfi  9301  elirrv  9556  kmlem2  10112  fin1a2lem10  10369  hsmexlem4  10389  iunfo  10499  modfsummodslem1  15765  lcmfunsnlem2lem1  16615  coprmprod  16638  coprmproddvdslem  16639  c0snmgmhm  20378  lbsextlem4  21078  frlmlbs  21713  coe1fzgsumdlem  22197  evl1gsumdlem  22250  maducoeval2  22534  dishaus  23276  dis2ndc  23354  dislly  23391  dissnlocfin  23423  comppfsc  23426  txdis  23526  txdis1cn  23529  txkgen  23546  isufil2  23802  alexsubALTlem4  23944  tmdgsum  23989  dscopn  24468  ovolfiniun  25409  volfiniun  25455  jensen  26906  uvtx01vtx  29331  cplgr1vlem  29363  unidifsnel  32471  gsumpart  33004  extdg1id  33668  irngss  33689  esum2dlem  34089  bnj1498  35058  funen1cnv  35085  wevgblacfn  35103  cvmlift2lem1  35296  funpartlem  35937  topdifinffinlem  37342  fvineqsneq  37407  pibt2  37412  finixpnum  37606  mbfresfi  37667  pclfinN  39901  sn-iotalem  42216  mzpcompact2lem  42746  dvmptfprod  45950  fourierdlem48  46159  sge0sup  46396  funressnvmo  47050  dfclnbgr6  47860  dfsclnbgr6  47862  termco  49474  termcarweu  49521  diag1f1o  49527  diag2f1o  49530