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

Theorem sstr2 3643
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 3630 . . . 4 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
21imim1d 82 . . 3 (𝐴𝐵 → ((𝑥𝐵𝑥𝐶) → (𝑥𝐴𝑥𝐶)))
32alimdv 1885 . 2 (𝐴𝐵 → (∀𝑥(𝑥𝐵𝑥𝐶) → ∀𝑥(𝑥𝐴𝑥𝐶)))
4 dfss2 3624 . 2 (𝐵𝐶 ↔ ∀𝑥(𝑥𝐵𝑥𝐶))
5 dfss2 3624 . 2 (𝐴𝐶 ↔ ∀𝑥(𝑥𝐴𝑥𝐶))
63, 4, 53imtr4g 285 1 (𝐴𝐵 → (𝐵𝐶𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1521  wcel 2030  wss 3607
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-in 3614  df-ss 3621
This theorem is referenced by:  sstr  3644  sstri  3645  sseq1  3659  sseq2  3660  ssun3  3811  ssun4  3812  ssinss1  3874  ssdisjOLD  4060  triun  4799  trintss  4802  sspwb  4947  exss  4961  frss  5110  relss  5240  funss  5945  funimass2  6010  fss  6094  suceloni  7055  limsssuc  7092  oaordi  7671  oeworde  7718  nnaordi  7743  sbthlem2  8112  sbthlem3  8113  sbthlem6  8116  domunfican  8274  fiint  8278  fiss  8371  dffi3  8378  inf3lem1  8563  trcl  8642  tcss  8658  ac10ct  8895  ackbij2lem4  9102  cfslb  9126  cfslbn  9127  cfcoflem  9132  coftr  9133  fin23lem15  9194  fin23lem20  9197  fin23lem36  9208  isf32lem1  9213  axdc3lem2  9311  ttukeylem2  9370  wunex2  9598  tskcard  9641  clsslem  13769  mrcss  16323  isacs2  16361  lubss  17168  frmdss2  17447  lsmlub  18124  lsslss  19009  lspss  19032  aspss  19380  mplcoe1  19513  mplcoe5  19516  ocv2ss  20065  ocvsscon  20067  lindsss  20211  lsslinds  20218  mdetunilem9  20474  tgss  20820  tgcl  20821  tgss3  20838  clsss  20906  ntrss  20907  neiss  20961  ssnei2  20968  opnnei  20972  cnpnei  21116  cnpco  21119  cncls  21126  cnprest  21141  hauscmp  21258  1stcfb  21296  1stcelcls  21312  reftr  21365  txcnpi  21459  txcnp  21471  txtube  21491  qtoptop2  21550  fgcl  21729  filssufilg  21762  ufileu  21770  uffix  21772  elfm2  21799  fmfnfmlem1  21805  fmco  21812  fbflim2  21828  flffbas  21846  flftg  21847  cnpflf2  21851  alexsubALTlem4  21901  neibl  22353  metcnp3  22392  xlebnum  22811  lebnumii  22812  caubl  23152  caublcls  23153  bcthlem2  23168  bcthlem5  23171  ovolsslem  23298  volsuplem  23369  dyadmbllem  23413  ellimc3  23688  limciun  23703  cpnord  23743  ubthlem1  27854  occon3  28284  chsupval  28322  chsupcl  28327  chsupss  28329  spanss  28335  chsupval2  28397  stlei  29227  dmdbr5  29295  mdsl0  29297  chrelat2i  29352  chirredlem1  29377  mdsymlem5  29394  mdsymlem6  29395  gsumle  29907  gsumvsca1  29910  gsumvsca2  29911  omsmon  30488  cvmliftlem15  31406  ss2mcls  31591  mclsax  31592  clsint2  32449  fgmin  32490  filnetlem4  32501  limsucncmpi  32569  bj-restpw  33170  bj-0int  33180  ptrecube  33539  heiborlem1  33740  heiborlem8  33747  pclssN  35498  dochexmidlem7  37072  incssnn0  37591  islssfg2  37958  hbtlem6  38016  hess  38391  psshepw  38399  clsf2  38741  sspwimpcf  39470  sspwimpcfVD  39471  dvmptfprod  40478  sprsymrelfo  42072  elbigo2  42671  setrec1lem2  42760  setrec1lem4  42762
  Copyright terms: Public domain W3C validator