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

Theorem sstr 3511
Description: Transitivity of subclasses. Theorem 6 of [Suppes] p. 23. (Contributed by NM, 5-Sep-2003.)
Assertion
Ref Expression
sstr

Proof of Theorem sstr
StepHypRef Expression
1 sstr2 3510 . 2
21imp 429 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  C_wss 3475
This theorem is referenced by:  sstrd  3513  sylan9ss  3516  ssdifss  3634  uneqin  3748  ssrnres  5450  relrelss  5536  fco  5746  fssres  5756  ssimaex  5938  dff3  6044  tpostpos2  6995  smores  7042  om00  7243  omeulem2  7251  pmss12g  7465  unblem1  7792  unblem2  7793  unblem3  7794  unblem4  7795  isfinite2  7798  cantnfval2  8109  cantnfle  8111  cantnfval2OLD  8139  cantnfleOLD  8141  rankxplim3  8320  alephinit  8497  dfac12lem2  8545  ackbij1lem11  8631  cfeq0  8657  cfsuc  8658  cff1  8659  cflim2  8664  cfss  8666  cfslb2n  8669  cofsmo  8670  cfsmolem  8671  fin23lem34  8747  fin1a2lem13  8813  axdc3lem2  8852  axdclem  8920  pwcfsdom  8979  wunfi  9120  tskxpss  9171  tskcard  9180  suprzcl  10967  uzwo  11173  uzwoOLD  11174  uzwo2  11175  infmssuzle  11193  infmssuzcl  11194  supxrbnd  11549  supxrgtmnf  11550  supxrre1  11551  supxrre2  11552  supxrss  11553  iccsupr  11646  hashf1lem2  12505  fsum2d  13586  fsumabs  13615  fsumrlim  13625  fsumo1  13626  fprod2d  13785  rpnnen2lem4  13951  rpnnen2lem7  13954  ramub2  14532  ressinbas  14693  ressress  14694  submre  15002  mrcss  15013  mreacs  15055  drsdirfi  15567  clatglbss  15757  ipopos  15790  cntz2ss  16370  ablfac1eulem  17123  subrgint  17451  tgval  19456  unitgOLD  19469  mretopd  19593  ssnei  19611  opnneiss  19619  restdis  19679  restcls  19682  restntr  19683  tgcnp  19754  fbssfi  20338  fgss2  20375  fgcl  20379  supfil  20396  alexsubALTlem3  20549  alexsubALTlem4  20550  cnextcn  20567  ustex3sym  20720  trust  20732  restutop  20740  utop2nei  20753  cfiluweak  20798  blssexps  20929  blssex  20930  mopni3  20997  metss  21011  metcnp3  21043  metustOLD  21070  metust  21071  cfilucfilOLD  21072  cfilucfil  21073  metutopOLD  21085  psmetutop  21086  tgioo  21301  xrsmopn  21317  fsumcn  21374  cncfmptid  21416  iscmet3lem2  21731  caussi  21736  ovolsslem  21895  ovolsscl  21897  ovolssnul  21898  opnmblALT  22012  itgfsum  22233  limcresi  22289  dvmptfsum  22376  plyss  22596  chsupunss  26262  shsupunss  26264  spanss  26266  shslubi  26303  shlub  26332  mdsl1i  27240  mdsl2i  27241  cvmdi  27243  mdslmd1lem1  27244  mdslmd1lem2  27245  mdslmd2i  27249  mdslmd4i  27252  atomli  27301  atcvatlem  27304  chirredlem2  27310  chirredi  27313  mdsymlem5  27326  xrge0infss  27580  tpr2rico  27894  sigainb  28136  dya2icoseg2  28249  eulerpartlemn  28320  ballotlem2  28427  cvmlift2lem12  28759  fin2so  30040  mblfinlem4  30054  ismblfin  30055  opnbnd  30143  fneint  30166  filbcmb  30231  heiborlem10  30316  igenmin  30461  isnacs3  30642  itgoss  31112  infmxrss  31492  islptre  31625  gsumlsscl  32976  lincellss  33027  ellcoellss  33036  sspwimp  33718  sspwimpVD  33719  lssatle  34740  paddss1  35541  paddss2  35542  paddss12  35543  paddssw2  35568  pclssN  35618  pclfinN  35624  polsubN  35631  2polvalN  35638  2polssN  35639  3polN  35640  2pmaplubN  35650  pnonsingN  35657  polsubclN  35676  dihord6apre  36983  dochsscl  37095  mapdordlem2  37364
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-in 3482  df-ss 3489
  Copyright terms: Public domain W3C validator