MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  snssi Unicode version

Theorem snssi 4174
Description: The singleton of an element of a class is a subset of the class. (Contributed by NM, 6-Jun-1994.)
Assertion
Ref Expression
snssi

Proof of Theorem snssi
StepHypRef Expression
1 snssg 4163 . 2
21ibi 241 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  e.wcel 1818  C_wss 3475  {csn 4029
This theorem is referenced by:  difsnid  4176  pwpw0  4178  sssn  4188  ssunsn2  4189  tpssi  4196  pwsnALT  4244  snelpwi  4697  intid  4710  xpsspw  5121  xpsspwOLD  5122  djussxp  5153  dmressnsn  5317  xpimasnOLD  5458  fconst6g  5779  dffv2  5946  fvimacnvi  6001  fvimacnvALT  6006  fsn2  6071  fsnunf  6109  suceloni  6648  curry1  6892  curry2  6895  ressuppss  6938  ressuppssdif  6940  mapsn  7480  ralxpmap  7488  fodomr  7688  sucdom2  7734  en1eqsn  7769  enp1ilem  7774  findcard2  7780  findcard2s  7781  marypha1lem  7913  marypha2lem1  7915  epfrs  8183  dfac5lem4  8528  kmlem11  8561  ackbij1lem2  8622  fin23lem26  8726  isfin1-3  8787  hsmexlem4  8830  axdc3lem4  8854  axresscn  9546  nn0ssre  10824  xrsupss  11529  supxrmnf  11538  1fv  11821  1exp  12195  hashxrcl  12429  hashdifsn  12477  brfi1indlem  12531  snopiswrd  12556  repsdf2  12750  modfsummods  13607  fsum00  13612  incexc  13649  xpnnenOLD  13943  2ebits  14097  bitsinvp1  14099  4sqlem19  14481  ramxrcl  14535  strlemor1  14724  mrcsncl  15009  acsfn1  15058  homaf  15357  dmcoass  15393  lubel  15752  gsumws1  16007  cycsubg2  16238  cntzsnval  16362  0frgp  16797  dpjidcl  17107  dpjidclOLD  17114  ablfac1eu  17124  lspsncl  17623  lspsnss  17636  lspsnid  17639  lpival  17893  lpiss  17898  lidldvgen  17903  znlidl  18570  znlidlOLD  18574  frgpcyg  18612  frlmlbs  18831  mat1dimelbas  18973  mat1dimmul  18978  smadiadetglem2  19174  isneip  19606  neips  19614  opnneip  19620  maxlp  19648  restsn2  19672  leordtval2  19713  ist1-3  19850  ordtt1  19880  2ndcdisj2  19958  uffix  20422  neiflim  20475  ptcmplem5  20556  cnextfres  20568  haustsms2  20635  ust0  20722  ustuqtop5  20748  dscopn  21094  icccmplem1  21327  bndth  21458  ovolsn  21906  icombl1  21973  plyun0  22594  coeeulem  22621  coeeu  22622  vieta1lem2  22707  aalioulem2  22729  taylfval  22754  perfectlem2  23505  istrkg2ld  23858  axlowdimlem7  24251  axlowdimlem10  24254  konigsberg  24987  hsn0elch  26166  chsupsn  26331  chsup0  26466  h1deoi  26467  h1dei  26468  h1did  26469  h1de2ctlem  26473  h1de2ci  26474  spansni  26475  spansnch  26478  elspansncl  26483  spansnpji  26496  spanunsni  26497  spanpr  26498  h1datomi  26499  spansnji  26564  h1da  27268  atom1d  27272  superpos  27273  esumnul  28059  esumcst  28071  hashf2  28090  measvuni  28185  cntnevol  28199  eulerpartlemt  28310  eulerpartlemmf  28314  eulerpartlemgh  28317  ballotlemfp1  28430  dfon2lem3  29217  altxpsspw  29627  mblfinlem2  30052  dvasin  30103  fdc  30238  prnc  30464  isfldidl  30465  ispridlc  30467  mapfzcons  30648  mzpcompact2lem  30684  diophrw  30692  binomcxplemnotnn0  31261  fprodsplit1f  31593  mccllem  31605  islptre  31625  cncfdmsn  31693  snmbl  31762  stoweidlem44  31826  fnbrafvb  32239  afvres  32257  mapsnop  32934  lincext2  33056  snlindsntorlem  33071  aacllem  33216  snelpwrVD  33631  bj-snglss  34528  islshpsm  34705  snatpsubN  35474  polatN  35655  atpsubclN  35669  pclfinclN  35674
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-v 3111  df-in 3482  df-ss 3489  df-sn 4030
  Copyright terms: Public domain W3C validator