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

Theorem sstr2 3574
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 3561 . . . 4 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
21imim1d 79 . . 3 (𝐴𝐵 → ((𝑥𝐵𝑥𝐶) → (𝑥𝐴𝑥𝐶)))
32alimdv 1831 . 2 (𝐴𝐵 → (∀𝑥(𝑥𝐵𝑥𝐶) → ∀𝑥(𝑥𝐴𝑥𝐶)))
4 dfss2 3556 . 2 (𝐵𝐶 ↔ ∀𝑥(𝑥𝐵𝑥𝐶))
5 dfss2 3556 . 2 (𝐴𝐶 ↔ ∀𝑥(𝑥𝐴𝑥𝐶))
63, 4, 53imtr4g 283 1 (𝐴𝐵 → (𝐵𝐶𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1472  wcel 1976  wss 3539
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-in 3546  df-ss 3553
This theorem is referenced by:  sstr  3575  sstri  3576  sseq1  3588  sseq2  3589  ssun3  3739  ssun4  3740  ssinss1  3802  ssdisjOLD  3978  triun  4688  trint0  4692  sspwb  4838  exss  4852  frss  4995  relss  5119  funss  5808  funimass2  5872  fss  5955  suceloni  6883  limsssuc  6920  oaordi  7491  oeworde  7538  nnaordi  7563  sbthlem2  7934  sbthlem3  7935  sbthlem6  7938  domunfican  8096  fiint  8100  fiss  8191  dffi3  8198  inf3lem1  8386  trcl  8465  tcss  8481  ac10ct  8718  ackbij2lem4  8925  cfslb  8949  cfslbn  8950  cfcoflem  8955  coftr  8956  fin23lem15  9017  fin23lem20  9020  fin23lem36  9031  isf32lem1  9036  axdc3lem2  9134  ttukeylem2  9193  wunex2  9417  tskcard  9460  clsslem  13520  mrcss  16048  isacs2  16086  lubss  16893  frmdss2  17172  lsmlub  17850  lsslss  18731  lspss  18754  aspss  19102  mplcoe1  19235  mplcoe5  19238  ocv2ss  19784  ocvsscon  19786  lindsss  19930  lsslinds  19937  mdetunilem9  20193  tgss  20531  tgcl  20532  tgss3  20549  clsss  20616  ntrss  20617  neiss  20671  ssnei2  20678  opnnei  20682  cnpnei  20826  cnpco  20829  cncls  20836  cnprest  20851  hauscmp  20968  1stcfb  21006  1stcelcls  21022  reftr  21075  txcnpi  21169  txcnp  21181  txtube  21201  qtoptop2  21260  fgcl  21440  filssufilg  21473  ufileu  21481  uffix  21483  elfm2  21510  fmfnfmlem1  21516  fmco  21523  fbflim2  21539  flffbas  21557  flftg  21558  cnpflf2  21562  alexsubALTlem4  21612  neibl  22064  metcnp3  22103  xlebnum  22520  lebnumii  22521  caubl  22859  caublcls  22860  bcthlem2  22875  bcthlem5  22878  ovolsslem  23004  volsuplem  23075  dyadmbllem  23118  ellimc3  23394  limciun  23409  cpnord  23449  ubthlem1  26944  occon3  27374  chsupval  27412  chsupcl  27417  chsupss  27419  spanss  27425  chsupval2  27487  stlei  28317  dmdbr5  28385  mdsl0  28387  chrelat2i  28442  chirredlem1  28467  mdsymlem5  28484  mdsymlem6  28485  gsumle  28944  gsumvsca1  28947  gsumvsca2  28948  omsmon  29521  cvmliftlem15  30368  ss2mcls  30553  mclsax  30554  clsint2  31328  fgmin  31369  filnetlem4  31380  limsucncmpi  31448  bj-restpw  32050  ptrecube  32403  heiborlem1  32604  heiborlem8  32611  pclssN  34022  dochexmidlem7  35597  incssnn0  36116  islssfg2  36483  hbtlem6  36542  hess  36918  psshepw  36926  clsf2  37268  sspwimpcf  38002  sspwimpcfVD  38003  dvmptfprod  38659  elbigo2  42166
  Copyright terms: Public domain W3C validator