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

Syntax hints:   → wi 4  ∀wal 1540   ∈ wcel 2114   ⊆ wss 3890

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

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

This theorem is referenced by:  sstr  3931  sstri  3932  sseq1  3948  sseq2  3949  ssun3  4121  ssun4  4122  ssinss1  4187  sspw  4553  triun  5207  trintss  5211  exss  5410  frss  5588  relss  5731  funss  6511  funimass2  6575  fss  6678  limsssuc  7794  oaordi  8474  oeworde  8522  nnaordi  8547  sbthlem2  9019  sbthlem3  9020  sbthlem6  9023  domunfican  9225  fiint  9230  fiss  9330  dffi3  9337  inf3lem1  9540  trcl  9640  tcss  9654  ac10ct  9947  ackbij2lem4  10154  cfslb  10179  cfslbn  10180  cfcoflem  10185  coftr  10186  fin23lem15  10247  fin23lem20  10250  fin23lem36  10261  isf32lem1  10266  axdc3lem2  10364  ttukeylem2  10423  wunex2  10652  tskcard  10695  clsslem  14937  mrcss  17573  isacs2  17610  lubss  18470  frmdss2  18822  lsmlub  19630  gsumle  20111  lsslss  20947  lspss  20970  ocv2ss  21663  ocvsscon  21665  lindsss  21814  lsslinds  21821  aspss  21866  mplcoe1  22025  mplcoe5  22028  mdetunilem9  22595  tgss  22943  tgcl  22944  tgss3  22961  clsss  23029  ntrss  23030  neiss  23084  ssnei2  23091  opnnei  23095  cnpnei  23239  cnpco  23242  cncls  23249  cnprest  23264  hauscmp  23382  1stcfb  23420  1stcelcls  23436  reftr  23489  txcnpi  23583  txcnp  23595  txtube  23615  qtoptop2  23674  fgcl  23853  filssufilg  23886  ufileu  23894  uffix  23896  elfm2  23923  fmfnfmlem1  23929  fmco  23936  fbflim2  23952  flffbas  23970  flftg  23971  cnpflf2  23975  alexsubALTlem4  24025  neibl  24476  metcnp3  24515  xlebnum  24942  lebnumii  24943  caubl  25285  caublcls  25286  bcthlem2  25302  bcthlem5  25305  ovolsslem  25461  volsuplem  25532  dyadmbllem  25576  ellimc3  25856  limciun  25871  cpnord  25912  precsexlem6  28218  precsexlem7  28219  ubthlem1  30956  occon3  31383  chsupval  31421  chsupcl  31426  chsupss  31428  spanss  31434  chsupval2  31496  stlei  32326  dmdbr5  32394  mdsl0  32396  chrelat2i  32451  chirredlem1  32476  mdsymlem5  32493  mdsymlem6  32494  gsumvsca1  33302  gsumvsca2  33303  omsmon  34458  cvmliftlem15  35496  ss2mcls  35766  mclsax  35767  clsint2  36527  fgmin  36568  filnetlem4  36579  limsucncmpi  36643  bj-restpw  37420  bj-0int  37429  rdgssun  37708  ptrecube  37955  heiborlem1  38146  heiborlem8  38153  refrelsredund4  39051  refrelredund4  39054  funALTVss  39119  pclssN  40354  dochexmidlem7  41926  incssnn0  43157  islssfg2  43517  hbtlem6  43575  hess  44225  psshepw  44233  clsf2  44571  mnuunid  44722  ismnushort  44746  sspwimpcf  45364  sspwimpcfVD  45365  dvmptfprod  46391  sprsymrelfo  47969  elbigo2  49040  subthinc  49930  setrec1lem2  50175  setrec1lem4  50177  setrec2mpt  50184