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

Theorem sstr2 3752
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 3739 . . . 4 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
21imim1d 82 . . 3 (𝐴𝐵 → ((𝑥𝐵𝑥𝐶) → (𝑥𝐴𝑥𝐶)))
32alimdv 1995 . 2 (𝐴𝐵 → (∀𝑥(𝑥𝐵𝑥𝐶) → ∀𝑥(𝑥𝐴𝑥𝐶)))
4 dfss2 3733 . 2 (𝐵𝐶 ↔ ∀𝑥(𝑥𝐵𝑥𝐶))
5 dfss2 3733 . 2 (𝐴𝐶 ↔ ∀𝑥(𝑥𝐴𝑥𝐶))
63, 4, 53imtr4g 285 1 (𝐴𝐵 → (𝐵𝐶𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1630  wcel 2140  wss 3716
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-clab 2748  df-cleq 2754  df-clel 2757  df-in 3723  df-ss 3730
This theorem is referenced by:  sstr  3753  sstri  3754  sseq1  3768  sseq2  3769  ssun3  3922  ssun4  3923  ssinss1  3985  ssdisjOLD  4172  triun  4919  trintss  4922  sspwb  5067  exss  5081  frss  5234  relss  5364  funss  6069  funimass2  6134  fss  6218  suceloni  7180  limsssuc  7217  oaordi  7798  oeworde  7845  nnaordi  7870  sbthlem2  8239  sbthlem3  8240  sbthlem6  8243  domunfican  8401  fiint  8405  fiss  8498  dffi3  8505  inf3lem1  8701  trcl  8780  tcss  8796  ac10ct  9068  ackbij2lem4  9277  cfslb  9301  cfslbn  9302  cfcoflem  9307  coftr  9308  fin23lem15  9369  fin23lem20  9372  fin23lem36  9383  isf32lem1  9388  axdc3lem2  9486  ttukeylem2  9545  wunex2  9773  tskcard  9816  clsslem  13945  mrcss  16499  isacs2  16536  lubss  17343  frmdss2  17622  lsmlub  18299  lsslss  19184  lspss  19207  aspss  19555  mplcoe1  19688  mplcoe5  19691  ocv2ss  20240  ocvsscon  20242  lindsss  20386  lsslinds  20393  mdetunilem9  20649  tgss  20995  tgcl  20996  tgss3  21013  clsss  21081  ntrss  21082  neiss  21136  ssnei2  21143  opnnei  21147  cnpnei  21291  cnpco  21294  cncls  21301  cnprest  21316  hauscmp  21433  1stcfb  21471  1stcelcls  21487  reftr  21540  txcnpi  21634  txcnp  21646  txtube  21666  qtoptop2  21725  fgcl  21904  filssufilg  21937  ufileu  21945  uffix  21947  elfm2  21974  fmfnfmlem1  21980  fmco  21987  fbflim2  22003  flffbas  22021  flftg  22022  cnpflf2  22026  alexsubALTlem4  22076  neibl  22528  metcnp3  22567  xlebnum  22986  lebnumii  22987  caubl  23327  caublcls  23328  bcthlem2  23343  bcthlem5  23346  ovolsslem  23473  volsuplem  23544  dyadmbllem  23588  ellimc3  23863  limciun  23878  cpnord  23918  ubthlem1  28057  occon3  28487  chsupval  28525  chsupcl  28530  chsupss  28532  spanss  28538  chsupval2  28600  stlei  29430  dmdbr5  29498  mdsl0  29500  chrelat2i  29555  chirredlem1  29580  mdsymlem5  29597  mdsymlem6  29598  gsumle  30110  gsumvsca1  30113  gsumvsca2  30114  omsmon  30691  cvmliftlem15  31609  ss2mcls  31794  mclsax  31795  clsint2  32652  fgmin  32693  filnetlem4  32704  limsucncmpi  32772  bj-restpw  33370  bj-0int  33380  ptrecube  33741  heiborlem1  33942  heiborlem8  33949  pclssN  35702  dochexmidlem7  37276  incssnn0  37795  islssfg2  38162  hbtlem6  38220  hess  38595  psshepw  38603  clsf2  38945  sspwimpcf  39674  sspwimpcfVD  39675  dvmptfprod  40682  sprsymrelfo  42276  elbigo2  42875  setrec1lem2  42964  setrec1lem4  42966
  Copyright terms: Public domain W3C validator