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

Theorem snssi 4472
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 4447 . 2 (𝐴𝐵 → (𝐴𝐵 ↔ {𝐴} ⊆ 𝐵))
21ibi 256 1 (𝐴𝐵 → {𝐴} ⊆ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2127  wss 3703  {csn 4309
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-v 3330  df-in 3710  df-ss 3717  df-sn 4310
This theorem is referenced by:  snssd  4473  difsnid  4474  eldifeldifsn  4475  pwpw0  4477  sssn  4491  ssunsn2  4492  tpssi  4502  pwsnALT  4569  snelpwi  5049  intid  5063  frirr  5231  xpsspw  5377  djussxp  5411  dmressnsn  5584  fconst6g  6243  f1sng  6327  dffv2  6421  fvimacnvi  6482  fvimacnvALT  6487  fsn2  6554  fsnunf  6603  abnexg  7117  suceloni  7166  curry1  7425  curry2  7428  ressuppss  7470  ressuppssdif  7472  mapsn  8053  ralxpmap  8061  fodomr  8264  sucdom2  8309  en1eqsn  8343  enp1ilem  8347  findcard2  8353  findcard2s  8354  marypha1lem  8492  marypha2lem1  8494  epfrs  8768  dfac5lem4  9110  kmlem11  9145  ackbij1lem2  9206  fin23lem26  9310  isfin1-3  9371  hsmexlem4  9414  axdc3lem4  9438  axresscn  10132  nn0ssre  11459  xrsupss  12303  supxrmnf  12311  1exp  13054  hashxrcl  13311  hashdifsn  13365  brfi1indlem  13441  repsdf2  13696  modfsummods  14695  fsum00  14700  incexc  14739  fprodsplit1f  14891  2ebits  15342  bitsinvp1  15344  lcmfunsnlem2lem1  15524  lcmfunsnlem2lem2  15525  lcmfunsnlem2  15526  coprmproddvdslem  15549  4sqlem19  15840  ramxrcl  15894  strlemor1OLD  16142  mrcsncl  16445  acsfn1  16494  homaf  16852  dmcoass  16888  lubel  17294  gsumws1  17548  cycsubg2  17803  cntzsnval  17928  0frgp  18363  dpjidcl  18628  ablfac1eu  18643  lspsncl  19150  lspsnss  19163  lspsnid  19166  lpival  19418  lpiss  19423  lidldvgen  19428  znlidl  20054  frlmlbs  20309  mat1dimelbas  20450  smadiadetglem2  20651  isneip  21082  neips  21090  opnneip  21096  maxlp  21124  restsn2  21148  leordtval2  21189  ist1-3  21326  ordtt1  21356  2ndcdisj2  21433  uffix  21897  neiflim  21950  ptcmplem5  22032  cnextfres1  22044  haustsms2  22112  ust0  22195  ustuqtop5  22221  dscopn  22550  icccmplem1  22797  bndth  22929  ovolsn  23434  icombl1  23502  plyun0  24123  coeeulem  24150  coeeu  24151  vieta1lem2  24236  aalioulem2  24258  taylfval  24283  perfectlem2  25125  istrkg2ld  25529  axlowdimlem7  25998  axlowdimlem10  26001  0clwlkv  27254  hsn0elch  28385  chsupsn  28552  chsup0  28687  h1deoi  28688  h1dei  28689  h1did  28690  h1de2ctlem  28694  h1de2ci  28695  spansni  28696  spansnch  28699  elspansncl  28704  spansnpji  28717  spanunsni  28718  spanpr  28719  h1datomi  28720  spansnji  28785  h1da  29488  atom1d  29492  superpos  29493  disjun0  29686  esumnul  30390  esumcst  30405  hashf2  30426  esum2d  30435  measvuni  30557  cntnevol  30571  eulerpartlemt  30713  eulerpartlemmf  30717  eulerpartlemgh  30720  ballotlemfp1  30833  reprinfz1  30980  dfon2lem3  31966  noextend  32096  noextendseq  32097  conway  32187  etasslt  32197  altxpsspw  32361  bj-snglss  33235  lindsenlbs  33686  poimirlem16  33707  poimirlem19  33710  poimirlem23  33714  poimirlem25  33716  poimirlem29  33720  poimirlem31  33722  mblfinlem2  33729  dvasin  33778  fdc  33823  prnc  34148  isfldidl  34149  ispridlc  34151  islshpsm  34739  snatpsubN  35508  polatN  35689  atpsubclN  35703  pclfinclN  35708  mapfzcons  37750  mzpcompact2lem  37785  diophrw  37793  brfvidRP  38451  cotrcltrcl  38488  corcltrcl  38502  cotrclrcl  38505  gneispa  38899  binomcxplemnotnn0  39026  snelpwrVD  39534  disjiun2  39694  mapsnd  39856  infxrpnf  40141  mccllem  40301  islptre  40323  cncfdmsn  40575  snmbl  40651  stoweidlem44  40733  sge0tsms  41069  sge0iunmptlemfi  41102  ismeannd  41156  isomenndlem  41219  hoidmvlelem3  41286  hoidmvlelem4  41287  ovnhoilem1  41290  fnbrafvb  41709  afvres  41727  perfectALTVlem2  42110  mapsnop  42602  lincext2  42723  snlindsntorlem  42738  aacllem  43029
  Copyright terms: Public domain W3C validator