Theorem sstr2 4015

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.) Avoid axioms. (Revised by GG, 19-May-2025.)

Assertion

Ref	Expression
sstr2	⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶))

Proof of Theorem sstr2

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		imim1 83	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)))
2	1	al2imi 1813	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶) → ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)))
3		df-ss 3993	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
4		df-ss 3993	. . 3 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶))
5		df-ss 3993	. . 3 ⊢ (𝐴 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶))
6	4, 5	imbi12i 350	. 2 ⊢ ((𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶) ↔ (∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶) → ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)))
7	2, 3, 6	3imtr4i 292	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶))

Syntax hints:   → wi 4  ∀wal 1535   ∈ wcel 2108   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807

This theorem depends on definitions:  df-bi 207  df-ss 3993

This theorem is referenced by:  sstr  4017  sstri  4018  sseq1  4034  sseq2  4035  ssun3  4203  ssun4  4204  ssinss1  4267  sspw  4633  triun  5298  trintss  5302  exss  5483  frss  5664  relss  5805  funss  6597  funimass2  6661  fss  6763  sucexeloniOLD  7846  suceloniOLD  7848  limsssuc  7887  oaordi  8602  oeworde  8649  nnaordi  8674  sbthlem2  9150  sbthlem3  9151  sbthlem6  9154  domunfican  9389  fiint  9394  fiintOLD  9395  fiss  9493  dffi3  9500  inf3lem1  9697  trcl  9797  tcss  9813  ac10ct  10103  ackbij2lem4  10310  cfslb  10335  cfslbn  10336  cfcoflem  10341  coftr  10342  fin23lem15  10403  fin23lem20  10406  fin23lem36  10417  isf32lem1  10422  axdc3lem2  10520  ttukeylem2  10579  wunex2  10807  tskcard  10850  clsslem  15033  mrcss  17674  isacs2  17711  lubss  18583  frmdss2  18898  lsmlub  19706  lsslss  20982  lspss  21005  ocv2ss  21714  ocvsscon  21716  lindsss  21867  lsslinds  21874  aspss  21920  mplcoe1  22078  mplcoe5  22081  mdetunilem9  22647  tgss  22996  tgcl  22997  tgss3  23014  clsss  23083  ntrss  23084  neiss  23138  ssnei2  23145  opnnei  23149  cnpnei  23293  cnpco  23296  cncls  23303  cnprest  23318  hauscmp  23436  1stcfb  23474  1stcelcls  23490  reftr  23543  txcnpi  23637  txcnp  23649  txtube  23669  qtoptop2  23728  fgcl  23907  filssufilg  23940  ufileu  23948  uffix  23950  elfm2  23977  fmfnfmlem1  23983  fmco  23990  fbflim2  24006  flffbas  24024  flftg  24025  cnpflf2  24029  alexsubALTlem4  24079  neibl  24535  metcnp3  24574  xlebnum  25016  lebnumii  25017  caubl  25361  caublcls  25362  bcthlem2  25378  bcthlem5  25381  ovolsslem  25538  volsuplem  25609  dyadmbllem  25653  ellimc3  25934  limciun  25949  cpnord  25991  precsexlem6  28254  precsexlem7  28255  ubthlem1  30902  occon3  31329  chsupval  31367  chsupcl  31372  chsupss  31374  spanss  31380  chsupval2  31442  stlei  32272  dmdbr5  32340  mdsl0  32342  chrelat2i  32397  chirredlem1  32422  mdsymlem5  32439  mdsymlem6  32440  gsumle  33074  gsumvsca1  33205  gsumvsca2  33206  omsmon  34263  cvmliftlem15  35266  ss2mcls  35536  mclsax  35537  clsint2  36295  fgmin  36336  filnetlem4  36347  limsucncmpi  36411  bj-restpw  37058  bj-0int  37067  rdgssun  37344  ptrecube  37580  heiborlem1  37771  heiborlem8  37778  refrelsredund4  38588  refrelredund4  38591  funALTVss  38655  pclssN  39851  dochexmidlem7  41423  incssnn0  42667  islssfg2  43028  hbtlem6  43086  hess  43742  psshepw  43750  clsf2  44088  mnuunid  44246  ismnushort  44270  sspwimpcf  44891  sspwimpcfVD  44892  dvmptfprod  45866  sprsymrelfo  47371  elbigo2  48286  subthinc  48707  setrec1lem2  48780  setrec1lem4  48782  setrec2mpt  48789