Theorem sstr2 3990

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 1815	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶) → ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)))
3		df-ss 3968	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
4		df-ss 3968	. . 3 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶))
5		df-ss 3968	. . 3 ⊢ (𝐴 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶))
6	4, 5	imbi12i 350	. 2 ⊢ ((𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶) ↔ (∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶) → ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)))
7	2, 3, 6	3imtr4i 292	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶))

Syntax hints:   → wi 4  ∀wal 1538   ∈ wcel 2108   ⊆ wss 3951

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

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

This theorem is referenced by:  sstr  3992  sstri  3993  sseq1  4009  sseq2  4010  ssun3  4180  ssun4  4181  ssinss1  4246  sspw  4611  triun  5274  trintss  5278  exss  5468  frss  5649  relss  5791  funss  6585  funimass2  6649  fss  6752  sucexeloniOLD  7830  suceloniOLD  7832  limsssuc  7871  oaordi  8584  oeworde  8631  nnaordi  8656  sbthlem2  9124  sbthlem3  9125  sbthlem6  9128  domunfican  9361  fiint  9366  fiintOLD  9367  fiss  9464  dffi3  9471  inf3lem1  9668  trcl  9768  tcss  9784  ac10ct  10074  ackbij2lem4  10281  cfslb  10306  cfslbn  10307  cfcoflem  10312  coftr  10313  fin23lem15  10374  fin23lem20  10377  fin23lem36  10388  isf32lem1  10393  axdc3lem2  10491  ttukeylem2  10550  wunex2  10778  tskcard  10821  clsslem  15023  mrcss  17659  isacs2  17696  lubss  18558  frmdss2  18876  lsmlub  19682  lsslss  20959  lspss  20982  ocv2ss  21691  ocvsscon  21693  lindsss  21844  lsslinds  21851  aspss  21897  mplcoe1  22055  mplcoe5  22058  mdetunilem9  22626  tgss  22975  tgcl  22976  tgss3  22993  clsss  23062  ntrss  23063  neiss  23117  ssnei2  23124  opnnei  23128  cnpnei  23272  cnpco  23275  cncls  23282  cnprest  23297  hauscmp  23415  1stcfb  23453  1stcelcls  23469  reftr  23522  txcnpi  23616  txcnp  23628  txtube  23648  qtoptop2  23707  fgcl  23886  filssufilg  23919  ufileu  23927  uffix  23929  elfm2  23956  fmfnfmlem1  23962  fmco  23969  fbflim2  23985  flffbas  24003  flftg  24004  cnpflf2  24008  alexsubALTlem4  24058  neibl  24514  metcnp3  24553  xlebnum  24997  lebnumii  24998  caubl  25342  caublcls  25343  bcthlem2  25359  bcthlem5  25362  ovolsslem  25519  volsuplem  25590  dyadmbllem  25634  ellimc3  25914  limciun  25929  cpnord  25971  precsexlem6  28236  precsexlem7  28237  ubthlem1  30889  occon3  31316  chsupval  31354  chsupcl  31359  chsupss  31361  spanss  31367  chsupval2  31429  stlei  32259  dmdbr5  32327  mdsl0  32329  chrelat2i  32384  chirredlem1  32409  mdsymlem5  32426  mdsymlem6  32427  gsumle  33101  gsumvsca1  33232  gsumvsca2  33233  omsmon  34300  cvmliftlem15  35303  ss2mcls  35573  mclsax  35574  clsint2  36330  fgmin  36371  filnetlem4  36382  limsucncmpi  36446  bj-restpw  37093  bj-0int  37102  rdgssun  37379  ptrecube  37627  heiborlem1  37818  heiborlem8  37825  refrelsredund4  38633  refrelredund4  38636  funALTVss  38700  pclssN  39896  dochexmidlem7  41468  incssnn0  42722  islssfg2  43083  hbtlem6  43141  hess  43793  psshepw  43801  clsf2  44139  mnuunid  44296  ismnushort  44320  sspwimpcf  44940  sspwimpcfVD  44941  dvmptfprod  45960  sprsymrelfo  47484  elbigo2  48473  subthinc  49092  setrec1lem2  49207  setrec1lem4  49209  setrec2mpt  49216