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

Theorem snssi 4147
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  |-  ( A  e.  B  ->  { A }  C_  B )

Proof of Theorem snssi
StepHypRef Expression
1 snssg 4136 . 2  |-  ( A  e.  B  ->  ( A  e.  B  <->  { A }  C_  B ) )
21ibi 244 1  |-  ( A  e.  B  ->  { A }  C_  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1870    C_ wss 3442   {csn 4002
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-v 3089  df-in 3449  df-ss 3456  df-sn 4003
This theorem is referenced by:  difsnid  4149  pwpw0  4151  sssn  4161  ssunsn2  4162  tpssi  4169  pwsnALT  4217  snelpwi  4667  intid  4680  xpsspw  4968  djussxp  5000  dmressnsn  5163  fconst6g  5789  dffv2  5954  fvimacnvi  6011  fvimacnvALT  6016  fsn2  6077  fsnunf  6117  suceloni  6654  curry1  6899  curry2  6902  ressuppss  6945  ressuppssdif  6947  mapsn  7521  ralxpmap  7529  fodomr  7729  sucdom2  7774  en1eqsn  7807  enp1ilem  7811  findcard2  7817  findcard2s  7818  marypha1lem  7953  marypha2lem1  7955  epfrs  8214  dfac5lem4  8555  kmlem11  8588  ackbij1lem2  8649  fin23lem26  8753  isfin1-3  8814  hsmexlem4  8857  axdc3lem4  8881  axresscn  9571  nn0ssre  10873  xrsupss  11594  supxrmnf  11603  1fv  11906  1exp  12298  hashxrcl  12536  hashdifsn  12586  brfi1indlem  12640  snopiswrd  12668  repsdf2  12866  modfsummods  13831  fsum00  13836  incexc  13873  fprodsplit1f  14022  2ebits  14395  bitsinvp1  14397  lcmfunsnlem2lem1  14582  lcmfunsnlem2lem2  14583  lcmfunsnlem2  14584  coprmproddvdslem  14650  4sqlem19  14876  ramxrcl  14938  strlemor1  15179  mrcsncl  15469  acsfn1  15518  homaf  15876  dmcoass  15912  lubel  16319  gsumws1  16574  cycsubg2  16805  cntzsnval  16929  0frgp  17364  dpjidcl  17626  ablfac1eu  17641  lspsncl  18135  lspsnss  18148  lspsnid  18151  lpival  18404  lpiss  18409  lidldvgen  18414  znlidl  19035  frgpcyg  19075  frlmlbs  19286  mat1dimelbas  19427  mat1dimmul  19432  smadiadetglem2  19628  isneip  20052  neips  20060  opnneip  20066  maxlp  20094  restsn2  20118  leordtval2  20159  ist1-3  20296  ordtt1  20326  2ndcdisj2  20403  uffix  20867  neiflim  20920  ptcmplem5  21002  cnextfres1  21014  haustsms2  21082  ust0  21165  ustuqtop5  21191  dscopn  21519  icccmplem1  21751  bndth  21882  ovolsn  22326  icombl1  22393  plyun0  23019  coeeulem  23046  coeeu  23047  vieta1lem2  23132  aalioulem2  23154  taylfval  23179  perfectlem2  24021  istrkg2ld  24371  axlowdimlem7  24824  axlowdimlem10  24827  konigsberg  25560  hsn0elch  26736  chsupsn  26901  chsup0  27036  h1deoi  27037  h1dei  27038  h1did  27039  h1de2ctlem  27043  h1de2ci  27044  spansni  27045  spansnch  27048  elspansncl  27053  spansnpji  27066  spanunsni  27067  spanpr  27068  h1datomi  27069  spansnji  27134  h1da  27837  atom1d  27841  superpos  27842  disjun0  28044  esumnul  28708  esumcst  28723  hashf2  28744  esum2d  28753  measvuni  28875  cntnevol  28889  eulerpartlemt  29030  eulerpartlemmf  29034  eulerpartlemgh  29037  ballotlemfp1  29150  dfon2lem3  30218  altxpsspw  30529  bj-snglss  31313  poimirlem16  31660  poimirlem19  31663  poimirlem23  31667  poimirlem25  31669  poimirlem26  31670  poimirlem29  31673  poimirlem31  31675  mblfinlem2  31682  dvasin  31732  fdc  31778  prnc  32004  isfldidl  32005  ispridlc  32007  islshpsm  32255  snatpsubN  33024  polatN  33205  atpsubclN  33219  pclfinclN  33224  mapfzcons  35267  mzpcompact2lem  35302  diophrw  35310  brfvidRP  35919  cotrcltrcl  35956  corcltrcl  35970  cotrclrcl  35973  binomcxplemnotnn0  36342  snelpwrVD  36867  disjiun2  37039  mccllem  37249  islptre  37271  cncfdmsn  37340  snmbl  37409  stoweidlem44  37474  sge0tsms  37756  sge0iunmptlemfi  37789  ismeannd  37814  fnbrafvb  38046  afvres  38064  perfectALTVlem2  38234  nnsum3primesprm  38275  mapsnop  38886  lincext2  39008  snlindsntorlem  39023  aacllem  39301
  Copyright terms: Public domain W3C validator