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

Theorem sstr2 3960
 Description: Transitivity of subclass relationship. 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 3946 . . . 4 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
21imim1d 82 . . 3 (𝐴𝐵 → ((𝑥𝐵𝑥𝐶) → (𝑥𝐴𝑥𝐶)))
32alimdv 1918 . 2 (𝐴𝐵 → (∀𝑥(𝑥𝐵𝑥𝐶) → ∀𝑥(𝑥𝐴𝑥𝐶)))
4 dfss2 3939 . 2 (𝐵𝐶 ↔ ∀𝑥(𝑥𝐵𝑥𝐶))
5 dfss2 3939 . 2 (𝐴𝐶 ↔ ∀𝑥(𝑥𝐴𝑥𝐶))
63, 4, 53imtr4g 299 1 (𝐴𝐵 → (𝐵𝐶𝐴𝐶))
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∀wal 1536   ∈ wcel 2115   ⊆ wss 3919 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-v 3482  df-in 3926  df-ss 3936 This theorem is referenced by:  sstr  3961  sstri  3962  sseq1  3978  sseq2  3979  ssun3  4136  ssun4  4137  ssinss1  4199  sspw  4535  triun  5171  trintss  5175  exss  5342  frss  5509  relss  5643  funss  6362  funimass2  6425  fss  6517  suceloni  7522  limsssuc  7559  oaordi  8168  oeworde  8215  nnaordi  8240  sbthlem2  8625  sbthlem3  8626  sbthlem6  8629  domunfican  8788  fiint  8792  fiss  8885  dffi3  8892  inf3lem1  9088  trcl  9167  tcss  9183  ac10ct  9458  ackbij2lem4  9662  cfslb  9686  cfslbn  9687  cfcoflem  9692  coftr  9693  fin23lem15  9754  fin23lem20  9757  fin23lem36  9768  isf32lem1  9773  axdc3lem2  9871  ttukeylem2  9930  wunex2  10158  tskcard  10201  clsslem  14344  mrcss  16887  isacs2  16924  lubss  17731  frmdss2  18028  lsmlub  18790  lsslss  19733  lspss  19756  aspss  20106  mplcoe1  20246  mplcoe5  20249  ocv2ss  20817  ocvsscon  20819  lindsss  20968  lsslinds  20975  mdetunilem9  21229  tgss  21576  tgcl  21577  tgss3  21594  clsss  21662  ntrss  21663  neiss  21717  ssnei2  21724  opnnei  21728  cnpnei  21872  cnpco  21875  cncls  21882  cnprest  21897  hauscmp  22015  1stcfb  22053  1stcelcls  22069  reftr  22122  txcnpi  22216  txcnp  22228  txtube  22248  qtoptop2  22307  fgcl  22486  filssufilg  22519  ufileu  22527  uffix  22529  elfm2  22556  fmfnfmlem1  22562  fmco  22569  fbflim2  22585  flffbas  22603  flftg  22604  cnpflf2  22608  alexsubALTlem4  22658  neibl  23111  metcnp3  23150  xlebnum  23573  lebnumii  23574  caubl  23915  caublcls  23916  bcthlem2  23932  bcthlem5  23935  ovolsslem  24091  volsuplem  24162  dyadmbllem  24206  ellimc3  24485  limciun  24500  cpnord  24541  ubthlem1  28656  occon3  29083  chsupval  29121  chsupcl  29126  chsupss  29128  spanss  29134  chsupval2  29196  stlei  30026  dmdbr5  30094  mdsl0  30096  chrelat2i  30151  chirredlem1  30176  mdsymlem5  30193  mdsymlem6  30194  gsumle  30757  gsumvsca1  30886  gsumvsca2  30887  omsmon  31613  cvmliftlem15  32602  ss2mcls  32872  mclsax  32873  clsint2  33734  fgmin  33775  filnetlem4  33786  limsucncmpi  33850  bj-restpw  34451  bj-0int  34461  rdgssun  34740  ptrecube  35002  heiborlem1  35194  heiborlem8  35201  refrelsredund4  35972  refrelredund4  35975  funALTVss  36037  pclssN  37135  dochexmidlem7  38707  incssnn0  39568  islssfg2  39931  hbtlem6  39989  hess  40398  psshepw  40406  clsf2  40748  mnuunid  40905  sspwimpcf  41546  sspwimpcfVD  41547  dvmptfprod  42513  sprsymrelfo  43940  elbigo2  44892  setrec1lem2  45144  setrec1lem4  45146
 Copyright terms: Public domain W3C validator