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

Theorem snssi 3759
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 3754 . 2  |-  ( A  e.  B  ->  ( A  e.  B  <->  { A }  C_  B ) )
21ibi 232 1  |-  ( A  e.  B  ->  { A }  C_  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1684    C_ wss 3152   {csn 3640
This theorem is referenced by:  difsnid  3761  pwpw0  3763  sssn  3772  ssunsn2  3773  pwsnALT  3822  snelpwi  4220  intid  4231  suceloni  4604  xpsspw  4797  xpsspwOLD  4798  djussxp  4829  fconst6g  5430  dffv2  5592  fvimacnvi  5639  fvimacnvALT  5644  fsn2  5698  fsnunf  5718  curry1  6210  curry2  6213  mapsn  6809  fodomr  7012  sucdom2  7057  en1eqsn  7088  enp1ilem  7092  findcard2  7098  findcard2s  7099  marypha1lem  7186  marypha2lem1  7188  epfrs  7413  dfac5lem4  7753  kmlem11  7786  ackbij1lem2  7847  fin23lem26  7951  isfin1-3  8012  hsmexlem4  8055  axdc3lem4  8079  axresscn  8770  nn0ssre  9969  xrsupss  10627  supxrmnf  10636  1exp  11131  hashxrcl  11351  s1cl  11441  fsum00  12256  incexclem  12295  incexc  12296  xpnnenOLD  12488  2ebits  12638  bitsinvp1  12640  4sqlem19  13010  ramxrcl  13064  strlemor1  13235  mrcsncl  13514  acsfn1  13563  homaf  13862  dmcoass  13898  lubel  14226  gsumws1  14462  cycsubg2  14654  cntzsnval  14800  0frgp  15088  dpjidcl  15293  ablfac1eu  15308  lspsncl  15734  lspsnss  15747  lspsnid  15750  lpival  15997  lpiss  16002  lidldvgen  16007  znlidl  16487  frgpcyg  16527  isneip  16842  neips  16850  opnneip  16856  maxlp  16878  restsn2  16902  leordtval2  16942  ist1-3  17077  ordtt1  17107  2ndcdisj2  17183  uffix  17616  neiflim  17669  ptcmplem5  17750  haustsms2  17819  dscopn  18096  icccmplem1  18327  bndth  18456  ovolsn  18854  icombl1  18920  plyun0  19579  coeeulem  19606  coeeu  19607  vieta1lem2  19691  aalioulem2  19713  taylfval  19738  perfectlem2  20469  hsn0elch  21827  chsupsn  21992  chsup0  22127  h1deoi  22128  h1dei  22129  h1did  22130  h1de2ctlem  22134  h1de2ci  22135  spansni  22136  spansnch  22139  elspansncl  22144  spansnpji  22157  spanunsni  22158  spanpr  22159  h1datomi  22160  spansnji  22225  h1da  22929  atom1d  22933  superpos  22934  cntnevol  23175  esumnul  23427  esumcst  23436  hashf2  23452  measvuni  23542  konigsberg  23911  dfon2lem3  24141  altxpsspw  24511  axlowdimlem7  24576  axlowdimlem10  24579  dvreasin  24923  splintx  25049  cbicp  25166  domrancur1b  25200  domrancur1c  25202  apnei  25520  osneisi  25531  istopxc  25548  conttnf2  25562  1iskle  25989  pgapspf  26052  fdc  26455  prnc  26692  isfldidl  26693  ispridlc  26695  ralxpmap  26761  mapfzcons  26793  mzpcompact2lem  26829  diophrw  26838  frlmlbs  27249  stoweidlem44  27793  dmressnsn  27983  funcoressn  27990  funressnfv  27991  fnbrafvb  28016  afvres  28034  snelpwrVD  28606  islshpsm  29170  snatpsubN  29939  polatN  30120  atpsubclN  30134  pclfinclN  30139
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-in 3159  df-ss 3166  df-sn 3646
  Copyright terms: Public domain W3C validator