Theorem sstr2 3983

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

Syntax hints:   → wi 4  ∀wal 1531   ∈ wcel 2098   ⊆ wss 3944

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

This theorem depends on definitions:  df-bi 206  df-ss 3961

This theorem is referenced by:  sstr  3985  sstri  3986  sseq1  4002  sseq2  4003  ssun3  4172  ssun4  4173  ssinss1  4236  sspw  4615  triun  5281  trintss  5285  exss  5465  frss  5645  relss  5783  funss  6573  funimass2  6637  fss  6739  sucexeloniOLD  7814  suceloniOLD  7816  limsssuc  7855  oaordi  8567  oeworde  8614  nnaordi  8639  sbthlem2  9109  sbthlem3  9110  sbthlem6  9113  domunfican  9346  fiint  9350  fiss  9449  dffi3  9456  inf3lem1  9653  trcl  9753  tcss  9769  ac10ct  10059  ackbij2lem4  10267  cfslb  10291  cfslbn  10292  cfcoflem  10297  coftr  10298  fin23lem15  10359  fin23lem20  10362  fin23lem36  10373  isf32lem1  10378  axdc3lem2  10476  ttukeylem2  10535  wunex2  10763  tskcard  10806  clsslem  14967  mrcss  17599  isacs2  17636  lubss  18508  frmdss2  18823  lsmlub  19631  lsslss  20857  lspss  20880  ocv2ss  21622  ocvsscon  21624  lindsss  21775  lsslinds  21782  aspss  21827  mplcoe1  21997  mplcoe5  22000  mdetunilem9  22566  tgss  22915  tgcl  22916  tgss3  22933  clsss  23002  ntrss  23003  neiss  23057  ssnei2  23064  opnnei  23068  cnpnei  23212  cnpco  23215  cncls  23222  cnprest  23237  hauscmp  23355  1stcfb  23393  1stcelcls  23409  reftr  23462  txcnpi  23556  txcnp  23568  txtube  23588  qtoptop2  23647  fgcl  23826  filssufilg  23859  ufileu  23867  uffix  23869  elfm2  23896  fmfnfmlem1  23902  fmco  23909  fbflim2  23925  flffbas  23943  flftg  23944  cnpflf2  23948  alexsubALTlem4  23998  neibl  24454  metcnp3  24493  xlebnum  24935  lebnumii  24936  caubl  25280  caublcls  25281  bcthlem2  25297  bcthlem5  25300  ovolsslem  25457  volsuplem  25528  dyadmbllem  25572  ellimc3  25852  limciun  25867  cpnord  25909  precsexlem6  28160  precsexlem7  28161  ubthlem1  30752  occon3  31179  chsupval  31217  chsupcl  31222  chsupss  31224  spanss  31230  chsupval2  31292  stlei  32122  dmdbr5  32190  mdsl0  32192  chrelat2i  32247  chirredlem1  32272  mdsymlem5  32289  mdsymlem6  32290  gsumle  32894  gsumvsca1  33025  gsumvsca2  33026  omsmon  34046  cvmliftlem15  35036  ss2mcls  35306  mclsax  35307  clsint2  35941  fgmin  35982  filnetlem4  35993  limsucncmpi  36057  bj-restpw  36699  bj-0int  36708  rdgssun  36985  ptrecube  37221  heiborlem1  37412  heiborlem8  37419  refrelsredund4  38231  refrelredund4  38234  funALTVss  38298  pclssN  39494  dochexmidlem7  41066  incssnn0  42270  islssfg2  42634  hbtlem6  42692  hess  43349  psshepw  43357  clsf2  43695  mnuunid  43853  ismnushort  43877  sspwimpcf  44498  sspwimpcfVD  44499  dvmptfprod  45468  sprsymrelfo  46971  elbigo2  47808  subthinc  48229  setrec1lem2  48302  setrec1lem4  48304  setrec2mpt  48311