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

Theorem sstr2 3199
Description: Transitivity of subclasses. Exercise 5 of [TakeutiZaring] p. 17. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
Assertion
Ref Expression
sstr2  |-  ( A 
C_  B  ->  ( B  C_  C  ->  A  C_  C ) )

Proof of Theorem sstr2
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 ssel 3187 . . . 4  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
21imim1d 69 . . 3  |-  ( A 
C_  B  ->  (
( x  e.  B  ->  x  e.  C )  ->  ( x  e.  A  ->  x  e.  C ) ) )
32alimdv 1611 . 2  |-  ( A 
C_  B  ->  ( A. x ( x  e.  B  ->  x  e.  C )  ->  A. x
( x  e.  A  ->  x  e.  C ) ) )
4 dfss2 3182 . 2  |-  ( B 
C_  C  <->  A. x
( x  e.  B  ->  x  e.  C ) )
5 dfss2 3182 . 2  |-  ( A 
C_  C  <->  A. x
( x  e.  A  ->  x  e.  C ) )
63, 4, 53imtr4g 261 1  |-  ( A 
C_  B  ->  ( B  C_  C  ->  A  C_  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1530    e. wcel 1696    C_ wss 3165
This theorem is referenced by:  sstr  3200  sstri  3201  sseq1  3212  sseq2  3213  ssun3  3353  ssun4  3354  ssinss1  3410  ssdisj  3517  triun  4142  trint0  4146  sspwb  4239  exss  4252  frss  4376  suceloni  4620  limsssuc  4657  relss  4791  funss  5289  funimass2  5342  fss  5413  tfrlem1  6407  oaordi  6560  oeworde  6607  nnaordi  6632  sbthlem1  6987  sbthlem2  6988  sbthlem3  6989  sbthlem6  6992  domunfican  7145  fiint  7149  fiss  7193  dffi3  7200  inf3lem1  7345  trcl  7426  tcss  7445  ac10ct  7677  ackbij2lem4  7884  cfslb  7908  cfslbn  7909  cfcoflem  7914  coftr  7915  fin23lem15  7976  fin23lem20  7979  fin23lem36  7990  isf32lem1  7995  axdc3lem2  8093  ttukeylem2  8153  wunex2  8376  tskcard  8419  mrcss  13534  isacs2  13571  lubss  14241  frmdss2  14501  lsmlub  14990  lsslss  15734  lspss  15757  aspss  16088  mplcoe1  16225  mplcoe2  16227  ocv2ss  16589  ocvsscon  16591  tgss  16722  tgcl  16723  tgss3  16740  clsss  16807  ntrss  16808  neiss  16862  ssnei2  16869  opnnei  16873  cnpnei  17009  cnpco  17012  cncls  17019  cnprest  17033  hauscmp  17150  1stcfb  17187  1stcelcls  17203  txcnpi  17318  txcnp  17330  txtube  17350  qtoptop2  17406  fgcl  17589  filssufilg  17622  ufileu  17630  uffix  17632  elfm2  17659  fmfnfmlem1  17665  fmco  17672  fbflim2  17688  flffbas  17706  flftg  17707  cnpflf2  17711  alexsubALTlem4  17760  neibl  18063  metcnp3  18102  xlebnum  18479  lebnumii  18480  caubl  18749  caublcls  18750  bcthlem2  18763  bcthlem5  18766  ovolsslem  18859  volsuplem  18928  dyadmbllem  18970  ellimc3  19245  limciun  19260  cpnord  19300  ubthlem1  21465  occon3  21892  chsupval  21930  chsupcl  21935  chsupss  21937  spanss  21943  chsupval2  22005  stlei  22836  dmdbr5  22904  mdsl0  22906  chrelat2i  22961  chirredlem1  22986  mdsymlem5  23003  mdsymlem6  23004  cvmliftlem15  23844  limsucncmpi  24956  inttrp  25211  inposet  25381  intopcoaconlem3b  25641  intopcoaconlem3  25642  exopcopn  25675  limptlimpr2lem2  25678  islimrs3  25684  lvsovso  25729  pgapspf  26155  clsint2  26350  reftr  26392  fgmin  26422  filnetlem4  26433  heiborlem1  26638  heiborlem8  26645  incssnn0  26889  islssfg2  27272  lindsss  27397  lsslinds  27404  hbtlem6  27436  sspwimpcf  29012  sspwimpcfVD  29013  sspwimpALT2  29021  pclssN  30705  dochexmidlem7  32278
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator