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

Theorem snssi 4276
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 4264 . 2 (𝐴𝐵 → (𝐴𝐵 ↔ {𝐴} ⊆ 𝐵))
21ibi 254 1 (𝐴𝐵 → {𝐴} ⊆ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1976  wss 3536  {csn 4121
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-v 3171  df-in 3543  df-ss 3550  df-sn 4122
This theorem is referenced by:  snssd  4277  difsnid  4278  pwpw0  4280  sssn  4292  ssunsn2  4293  tpssi  4301  pwsnALT  4358  snelpwi  4831  intid  4844  frirr  5002  xpsspw  5142  djussxp  5174  dmressnsn  5342  fconst6g  5989  f1sng  6072  dffv2  6163  fvimacnvi  6221  fvimacnvALT  6226  fsn2  6291  fsnunf  6331  suceloni  6879  curry1  7130  curry2  7133  ressuppss  7175  ressuppssdif  7177  mapsn  7759  ralxpmap  7767  fodomr  7970  sucdom2  8015  en1eqsn  8049  enp1ilem  8053  findcard2  8059  findcard2s  8060  marypha1lem  8196  marypha2lem1  8198  epfrs  8464  dfac5lem4  8806  kmlem11  8839  ackbij1lem2  8900  fin23lem26  9004  isfin1-3  9065  hsmexlem4  9108  axdc3lem4  9132  axresscn  9822  nn0ssre  11140  xrsupss  11964  supxrmnf  11972  1exp  12703  hashxrcl  12959  hashdifsn  13012  brfi1indlem  13076  repsdf2  13319  modfsummods  14309  fsum00  14314  incexc  14351  fprodsplit1f  14503  2ebits  14950  bitsinvp1  14952  lcmfunsnlem2lem1  15132  lcmfunsnlem2lem2  15133  lcmfunsnlem2  15134  coprmproddvdslem  15157  4sqlem19  15448  ramxrcl  15502  strlemor1  15739  mrcsncl  16038  acsfn1  16088  homaf  16446  dmcoass  16482  lubel  16888  gsumws1  17142  cycsubg2  17397  cntzsnval  17523  0frgp  17958  dpjidcl  18223  ablfac1eu  18238  lspsncl  18741  lspsnss  18754  lspsnid  18757  lpival  19009  lpiss  19014  lidldvgen  19019  znlidl  19642  frlmlbs  19894  mat1dimelbas  20035  smadiadetglem2  20236  isneip  20658  neips  20666  opnneip  20672  maxlp  20700  restsn2  20724  leordtval2  20765  ist1-3  20902  ordtt1  20932  2ndcdisj2  21009  uffix  21474  neiflim  21527  ptcmplem5  21609  cnextfres1  21621  haustsms2  21689  ust0  21772  ustuqtop5  21798  dscopn  22126  icccmplem1  22362  bndth  22493  ovolsn  22984  icombl1  23052  plyun0  23671  coeeulem  23698  coeeu  23699  vieta1lem2  23784  aalioulem2  23806  taylfval  23831  perfectlem2  24669  istrkg2ld  25073  axlowdimlem7  25543  axlowdimlem10  25546  konigsberg  26277  hsn0elch  27292  chsupsn  27459  chsup0  27594  h1deoi  27595  h1dei  27596  h1did  27597  h1de2ctlem  27601  h1de2ci  27602  spansni  27603  spansnch  27606  elspansncl  27611  spansnpji  27624  spanunsni  27625  spanpr  27626  h1datomi  27627  spansnji  27692  h1da  28395  atom1d  28399  superpos  28400  disjun0  28593  esumnul  29240  esumcst  29255  hashf2  29276  esum2d  29285  measvuni  29407  cntnevol  29421  eulerpartlemt  29563  eulerpartlemmf  29567  eulerpartlemgh  29570  ballotlemfp1  29683  dfon2lem3  30737  altxpsspw  31057  bj-snglss  31951  lindsenlbs  32374  poimirlem16  32395  poimirlem19  32398  poimirlem23  32402  poimirlem25  32404  poimirlem29  32408  poimirlem31  32410  mblfinlem2  32417  dvasin  32466  fdc  32511  prnc  32836  isfldidl  32837  ispridlc  32839  islshpsm  33085  snatpsubN  33854  polatN  34035  atpsubclN  34049  pclfinclN  34054  mapfzcons  36097  mzpcompact2lem  36132  diophrw  36140  brfvidRP  36799  cotrcltrcl  36836  corcltrcl  36850  cotrclrcl  36853  gneispa  37248  binomcxplemnotnn0  37377  snelpwrVD  37888  disjiun2  38051  mapsnd  38183  mccllem  38465  islptre  38487  cncfdmsn  38577  snmbl  38656  stoweidlem44  38738  sge0tsms  39074  sge0iunmptlemfi  39107  ismeannd  39161  isomenndlem  39221  hoidmvlelem3  39288  hoidmvlelem4  39289  ovnhoilem1  39292  fnbrafvb  39685  afvres  39703  perfectALTVlem2  39967  mapsnop  41915  lincext2  42037  snlindsntorlem  42052  aacllem  42316
  Copyright terms: Public domain W3C validator