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

Theorem snssi 4726
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 4702 . 2 (𝐴𝐵 → (𝐴𝐵 ↔ {𝐴} ⊆ 𝐵))
21ibi 270 1 (𝐴𝐵 → {𝐴} ⊆ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2115  wss 3919  {csn 4550
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-12 2179  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1086  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-v 3482  df-in 3926  df-ss 3936  df-sn 4551
This theorem is referenced by:  snssd  4727  difsnid  4728  eldifeldifsn  4729  pwpw0  4731  sssn  4744  ssunsn2  4745  tpssi  4754  pwsnOLD  4818  snelpwi  5325  intid  5338  frirr  5520  xpsspw  5670  djussxp  5704  dmressnsn  5882  fconst6g  6557  f1sng  6645  dffv2  6745  fvimacnvi  6811  fvimacnvALT  6816  fsn2  6887  fsnunf  6936  abnexg  7469  suceloni  7519  curry1  7791  curry2  7794  ressuppss  7841  ressuppssdif  7843  mapsnd  8442  ralxpmap  8452  sucdom2  8619  fodomr  8661  en1eqsn  8741  enp1ilem  8745  findcard2  8751  findcard2s  8752  marypha1lem  8890  marypha2lem1  8892  epfrs  9166  dfac5lem4  9546  kmlem11  9580  ackbij1lem2  9637  fin23lem26  9741  isfin1-3  9802  hsmexlem4  9845  axdc3lem4  9869  axresscn  10564  nn0ssre  11896  nn0sscn  11897  xrsupss  12697  supxrmnf  12705  1exp  13461  hashxrcl  13721  hashdifsn  13778  hashdifsnp1  13857  repsdf2  14138  modfsummods  15146  fsum00  15151  incexc  15190  2ebits  15792  bitsinvp1  15794  lcmfunsnlem2lem1  15978  lcmfunsnlem2lem2  15979  lcmfunsnlem2  15980  coprmproddvdslem  16002  4sqlem19  16295  ramxrcl  16349  mrcsncl  16881  acsfn1  16930  homaf  17288  dmcoass  17324  lubel  17730  gsumws1  18000  cycsubg2  18351  cntzsnval  18452  0frgp  18903  dpjidcl  19178  ablfac1eu  19193  lspsncl  19744  lspsnss  19757  lspsnid  19760  lpival  20013  lpiss  20018  lidldvgen  20023  znlidl  20675  frlmlbs  20936  mat1dimelbas  21075  smadiadetglem2  21276  isneip  21708  neips  21716  opnneip  21722  maxlp  21750  restsn2  21774  leordtval2  21815  ist1-3  21952  ordtt1  21982  2ndcdisj2  22060  uffix  22524  neiflim  22577  ptcmplem5  22659  cnextfres1  22671  haustsms2  22740  ust0  22823  ustuqtop5  22849  dscopn  23178  icccmplem1  23425  bndth  23561  ovolsn  24097  icombl1  24165  plyun0  24792  coeeulem  24819  coeeu  24820  vieta1lem2  24905  aalioulem2  24927  taylfval  24952  perfectlem2  25812  istrkg2ld  26252  axlowdimlem7  26740  axlowdimlem10  26743  0clwlkv  27914  hsn0elch  29029  chsupsn  29194  chsup0  29329  h1deoi  29330  h1dei  29331  h1did  29332  h1de2ctlem  29336  h1de2ci  29337  spansni  29338  spansnch  29341  elspansncl  29346  spansnpji  29359  spanunsni  29360  spanpr  29361  h1datomi  29362  spansnji  29427  h1da  30130  atom1d  30134  superpos  30135  disjun0  30351  mptprop  30440  pwrssmgc  30686  rspsnid  30964  lindssn  30967  lbslsat  31044  esumnul  31334  esumcst  31349  hashf2  31370  esum2d  31379  measvuni  31500  cntnevol  31514  eulerpartlemt  31656  eulerpartlemmf  31660  eulerpartlemgh  31663  ballotlemfp1  31776  reprinfz1  31920  f1resfz0f1d  32388  dfon2lem3  33057  noextend  33200  noextendseq  33201  conway  33291  etasslt  33301  altxpsspw  33465  bj-snglss  34320  lindsadd  34962  lindsenlbs  34964  poimirlem16  34985  poimirlem19  34988  poimirlem23  34992  poimirlem25  34994  poimirlem29  34998  poimirlem31  35000  mblfinlem2  35007  dvasin  35053  fdc  35095  prnc  35417  isfldidl  35418  ispridlc  35420  islshpsm  36188  snatpsubN  36958  polatN  37139  atpsubclN  37153  pclfinclN  37158  mapfzcons  39513  mzpcompact2lem  39548  diophrw  39556  brfvidRP  40245  cotrcltrcl  40282  corcltrcl  40296  cotrclrcl  40299  gneispa  40692  binomcxplemnotnn0  40920  snelpwrVD  41397  disjiun2  41552  infxrpnf  41950  mccllem  42105  islptre  42127  cncfdmsn  42398  snmbl  42471  stoweidlem44  42552  sge0tsms  42885  sge0iunmptlemfi  42918  ismeannd  42972  isomenndlem  43035  hoidmvlelem3  43102  hoidmvlelem4  43103  ovnhoilem1  43106  fnbrafvb  43576  afvres  43594  afv2res  43661  perfectALTVlem2  44106  mapsnop  44612  lincext2  44729  snlindsntorlem  44744  aacllem  45183
  Copyright terms: Public domain W3C validator