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

Theorem snssi 4337
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 4325 . 2 (𝐴𝐵 → (𝐴𝐵 ↔ {𝐴} ⊆ 𝐵))
21ibi 256 1 (𝐴𝐵 → {𝐴} ⊆ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1989  wss 3572  {csn 4175
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-v 3200  df-in 3579  df-ss 3586  df-sn 4176
This theorem is referenced by:  snssd  4338  difsnid  4339  eldifeldifsn  4340  pwpw0  4342  sssn  4356  ssunsn2  4357  tpssi  4367  pwsnALT  4427  snelpwi  4910  intid  4924  frirr  5089  xpsspw  5231  djussxp  5265  dmressnsn  5436  fconst6g  6092  f1sng  6176  dffv2  6269  fvimacnvi  6329  fvimacnvALT  6334  fsn2  6400  fsnunf  6448  abnexg  6961  suceloni  7010  curry1  7266  curry2  7269  ressuppss  7311  ressuppssdif  7313  mapsn  7896  ralxpmap  7904  fodomr  8108  sucdom2  8153  en1eqsn  8187  enp1ilem  8191  findcard2  8197  findcard2s  8198  marypha1lem  8336  marypha2lem1  8338  epfrs  8604  dfac5lem4  8946  kmlem11  8979  ackbij1lem2  9040  fin23lem26  9144  isfin1-3  9205  hsmexlem4  9248  axdc3lem4  9272  axresscn  9966  nn0ssre  11293  xrsupss  12136  supxrmnf  12144  1exp  12884  hashxrcl  13143  hashdifsn  13197  brfi1indlem  13273  repsdf2  13519  modfsummods  14519  fsum00  14524  incexc  14563  fprodsplit1f  14715  2ebits  15163  bitsinvp1  15165  lcmfunsnlem2lem1  15345  lcmfunsnlem2lem2  15346  lcmfunsnlem2  15347  coprmproddvdslem  15370  4sqlem19  15661  ramxrcl  15715  strlemor1OLD  15963  mrcsncl  16266  acsfn1  16316  homaf  16674  dmcoass  16710  lubel  17116  gsumws1  17370  cycsubg2  17625  cntzsnval  17751  0frgp  18186  dpjidcl  18451  ablfac1eu  18466  lspsncl  18971  lspsnss  18984  lspsnid  18987  lpival  19239  lpiss  19244  lidldvgen  19249  znlidl  19875  frlmlbs  20130  mat1dimelbas  20271  smadiadetglem2  20472  isneip  20903  neips  20911  opnneip  20917  maxlp  20945  restsn2  20969  leordtval2  21010  ist1-3  21147  ordtt1  21177  2ndcdisj2  21254  uffix  21719  neiflim  21772  ptcmplem5  21854  cnextfres1  21866  haustsms2  21934  ust0  22017  ustuqtop5  22043  dscopn  22372  icccmplem1  22619  bndth  22751  ovolsn  23257  icombl1  23325  plyun0  23947  coeeulem  23974  coeeu  23975  vieta1lem2  24060  aalioulem2  24082  taylfval  24107  perfectlem2  24949  istrkg2ld  25353  axlowdimlem7  25822  axlowdimlem10  25825  hsn0elch  28089  chsupsn  28256  chsup0  28391  h1deoi  28392  h1dei  28393  h1did  28394  h1de2ctlem  28398  h1de2ci  28399  spansni  28400  spansnch  28403  elspansncl  28408  spansnpji  28421  spanunsni  28422  spanpr  28423  h1datomi  28424  spansnji  28489  h1da  29192  atom1d  29196  superpos  29197  disjun0  29392  esumnul  30095  esumcst  30110  hashf2  30131  esum2d  30140  measvuni  30262  cntnevol  30276  eulerpartlemt  30418  eulerpartlemmf  30422  eulerpartlemgh  30425  ballotlemfp1  30538  reprinfz1  30685  dfon2lem3  31674  noextend  31803  noextendseq  31804  conway  31894  etasslt  31904  altxpsspw  32068  bj-snglss  32942  lindsenlbs  33384  poimirlem16  33405  poimirlem19  33408  poimirlem23  33412  poimirlem25  33414  poimirlem29  33418  poimirlem31  33420  mblfinlem2  33427  dvasin  33476  fdc  33521  prnc  33846  isfldidl  33847  ispridlc  33849  islshpsm  34093  snatpsubN  34862  polatN  35043  atpsubclN  35057  pclfinclN  35062  mapfzcons  37105  mzpcompact2lem  37140  diophrw  37148  brfvidRP  37806  cotrcltrcl  37843  corcltrcl  37857  cotrclrcl  37860  gneispa  38254  binomcxplemnotnn0  38381  snelpwrVD  38892  disjiun2  39052  mapsnd  39210  infxrpnf  39493  mccllem  39635  islptre  39657  cncfdmsn  39872  snmbl  39948  stoweidlem44  40030  sge0tsms  40366  sge0iunmptlemfi  40399  ismeannd  40453  isomenndlem  40513  hoidmvlelem3  40580  hoidmvlelem4  40581  ovnhoilem1  40584  fnbrafvb  41003  afvres  41021  perfectALTVlem2  41402  mapsnop  41894  lincext2  42015  snlindsntorlem  42030  aacllem  42318
  Copyright terms: Public domain W3C validator