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

Theorem sstr2 3510
Description: Transitivity of subclasses. Exercise 5 of [TakeutiZaring] p. 17. (Contributed by NM, 24-Jun-1993.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
Assertion
Ref Expression
sstr2

Proof of Theorem sstr2
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 ssel 3497 . . . 4
21imim1d 75 . . 3
32alimdv 1709 . 2
4 dfss2 3492 . 2
5 dfss2 3492 . 2
63, 4, 53imtr4g 270 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  A.wal 1393  e.wcel 1818  C_wss 3475
This theorem is referenced by:  sstr  3511  sstri  3512  sseq1  3524  sseq2  3525  ssun3  3668  ssun4  3669  ssinss1  3725  ssdisj  3876  triun  4558  trint0  4562  sspwb  4701  exss  4715  frss  4851  relss  5095  funss  5611  funimass2  5667  fss  5744  suceloni  6648  limsssuc  6685  oaordi  7214  oeworde  7261  nnaordi  7286  sbthlem2  7648  sbthlem3  7649  sbthlem6  7652  domunfican  7813  fiint  7817  fiss  7904  dffi3  7911  inf3lem1  8066  trcl  8180  tcss  8196  ac10ct  8436  ackbij2lem4  8643  cfslb  8667  cfslbn  8668  cfcoflem  8673  coftr  8674  fin23lem15  8735  fin23lem20  8738  fin23lem36  8749  isf32lem1  8754  axdc3lem2  8852  ttukeylem2  8911  wunex2  9137  tskcard  9180  mrcss  15013  isacs2  15050  lubss  15751  frmdss2  16031  lsmlub  16683  lsslss  17607  lspss  17630  aspss  17981  mplcoe1  18127  mplcoe5  18131  mplcoe2OLD  18133  ocv2ss  18704  ocvsscon  18706  lindsss  18859  lsslinds  18866  mdetunilem9  19122  tgss  19470  tgcl  19471  tgss3  19488  clsss  19555  ntrss  19556  neiss  19610  ssnei2  19617  opnnei  19621  cnpnei  19765  cnpco  19768  cncls  19775  cnprest  19790  hauscmp  19907  1stcfb  19946  1stcelcls  19962  reftr  20015  txcnpi  20109  txcnp  20121  txtube  20141  qtoptop2  20200  fgcl  20379  filssufilg  20412  ufileu  20420  uffix  20422  elfm2  20449  fmfnfmlem1  20455  fmco  20462  fbflim2  20478  flffbas  20496  flftg  20497  cnpflf2  20501  alexsubALTlem4  20550  neibl  21004  metcnp3  21043  xlebnum  21465  lebnumii  21466  caubl  21746  caublcls  21747  bcthlem2  21764  bcthlem5  21767  ovolsslem  21895  volsuplem  21965  dyadmbllem  22008  ellimc3  22283  limciun  22298  cpnord  22338  ubthlem1  25786  occon3  26215  chsupval  26253  chsupcl  26258  chsupss  26260  spanss  26266  chsupval2  26328  stlei  27159  dmdbr5  27227  mdsl0  27229  chrelat2i  27284  chirredlem1  27309  mdsymlem5  27326  mdsymlem6  27327  gsumle  27770  gsumvsca1  27773  gsumvsca2  27774  omsmon  28267  cvmliftlem15  28743  ss2mcls  28928  mclsax  28929  limsucncmpi  29910  clsint2  30147  fgmin  30188  filnetlem4  30199  heiborlem1  30307  heiborlem8  30314  incssnn0  30643  islssfg2  31017  hbtlem6  31078  dvmptfprod  31742  sspwimpcf  33720  sspwimpcfVD  33721  pclssN  35618  dochexmidlem7  37193  hess  37803  psshepw  37811
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