Theorem sstr2 3929

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

Syntax hints:   → wi 4  ∀wal 1545   ∈ wcel 2119   ⊆ wss 3890

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

This theorem depends on definitions:  df-bi 208  df-ss 3907

This theorem is referenced by:  sstr  3930  sstri  3931  sseq1  3947  sseq2  3948  ssun3  4116  ssun4  4117  ssinss1  4181  sspw  4547  triun  5201  trintss  5205  exss  5409  frss  5589  relss  5732  funss  6511  funimass2  6575  fss  6678  limsssuc  7797  oaordi  8478  oeworde  8526  nnaordi  8551  sbthlem2  9023  sbthlem3  9024  sbthlem6  9027  domunfican  9229  fiint  9234  fiss  9334  dffi3  9341  inf3lem1  9547  trcl  9647  tcss  9661  ac10ct  9954  ackbij2lem4  10161  cfslb  10186  cfslbn  10187  cfcoflem  10192  coftr  10193  fin23lem15  10254  fin23lem20  10257  fin23lem36  10268  isf32lem1  10273  axdc3lem2  10371  ttukeylem2  10430  wunex2  10659  tskcard  10702  clsslem  14944  mrcss  17580  isacs2  17617  lubss  18477  frmdss2  18829  lsmlub  19637  gsumle  20118  lsslss  20958  lspss  20981  ocv2ss  21655  ocvsscon  21657  lindsss  21806  lsslinds  21813  aspss  21858  mplcoe1  22020  mplcoe5  22023  mdetunilem9  22610  tgss  22958  tgcl  22959  tgss3  22976  clsss  23044  ntrss  23045  neiss  23099  ssnei2  23106  opnnei  23110  cnpnei  23254  cnpco  23257  cncls  23264  cnprest  23279  hauscmp  23397  1stcfb  23435  1stcelcls  23451  reftr  23504  txcnpi  23598  txcnp  23610  txtube  23630  qtoptop2  23689  fgcl  23868  filssufilg  23901  ufileu  23909  uffix  23911  elfm2  23938  fmfnfmlem1  23944  fmco  23951  fbflim2  23967  flffbas  23985  flftg  23986  cnpflf2  23990  alexsubALTlem4  24040  neibl  24491  metcnp3  24530  xlebnum  24957  lebnumii  24958  caubl  25300  caublcls  25301  bcthlem2  25317  bcthlem5  25320  ovolsslem  25476  volsuplem  25547  dyadmbllem  25591  ellimc3  25871  limciun  25886  cpnord  25927  precsexlem6  28229  precsexlem7  28230  ubthlem1  30966  occon3  31393  chsupval  31431  chsupcl  31436  chsupss  31438  spanss  31444  chsupval2  31506  stlei  32336  dmdbr5  32404  mdsl0  32406  chrelat2i  32461  chirredlem1  32486  mdsymlem5  32503  mdsymlem6  32504  gsumvsca1  33314  gsumvsca2  33315  omsmon  34489  cvmliftlem15  35533  ss2mcls  35803  mclsax  35804  clsint2  36564  fgmin  36605  filnetlem4  36616  limsucncmpi  36680  bj-restpw  37457  bj-0int  37466  rdgssun  37747  ptrecube  37994  heiborlem1  38185  heiborlem8  38192  refrelsredund4  39090  refrelredund4  39093  funALTVss  39158  pclssN  40393  dochexmidlem7  41965  incssnn0  43167  islssfg2  43523  hbtlem6  43581  hess  44231  psshepw  44239  clsf2  44577  mnuunid  44728  ismnushort  44752  sspwimpcf  45370  sspwimpcfVD  45371  dvmptfprod  46395  sprsymrelfo  47979  elbigo2  49050  subthinc  49940  setrec1lem2  50185  setrec1lem4  50187  setrec2mpt  50194