Theorem sstr2 3943

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

Syntax hints:   → wi 4  ∀wal 1557   ∈ wcel 2141   ⊆ wss 3904

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

This theorem depends on definitions:  df-bi 209  df-ss 3921

This theorem is referenced by:  sstr  3944  sstri  3945  sseq1  3961  sseq2  3962  ssun3  4132  ssun4  4133  ssinss1OLD  4198  sspw  4565  triun  5221  trintss  5225  exss  5429  frss  5609  relss  5752  funss  6536  funimass2  6600  fss  6704  limsssuc  7826  oaordi  8510  oeworde  8558  nnaordi  8583  sbthlem2  9056  sbthlem3  9057  sbthlem6  9060  domunfican  9262  fiint  9267  fiss  9367  dffi3  9374  inf3lem1  9580  trcl  9680  tcss  9694  ac10ct  9987  ackbij2lem4  10194  cfslb  10220  cfslbn  10221  cfcoflem  10226  coftr  10227  fin23lem15  10288  fin23lem20  10291  fin23lem36  10302  isf32lem1  10307  axdc3lem2  10405  ttukeylem2  10464  wunex2  10693  tskcard  10736  clsslem  14994  mrcss  17631  isacs2  17668  lubss  18528  frmdss2  18880  lsmlub  19687  gsumle  20168  lsslss  21008  lspss  21031  ocv2ss  21705  ocvsscon  21707  lindsss  21856  lsslinds  21863  aspss  21908  mplcoe1  22070  mplcoe5  22073  mdetunilem9  22660  tgss  23008  tgcl  23009  tgss3  23026  clsss  23094  ntrss  23095  neiss  23149  ssnei2  23156  opnnei  23160  cnpnei  23304  cnpco  23307  cncls  23314  cnprest  23329  hauscmp  23447  1stcfb  23485  1stcelcls  23501  reftr  23554  txcnpi  23648  txcnp  23660  txtube  23680  qtoptop2  23739  fgcl  23918  filssufilg  23951  ufileu  23959  uffix  23961  elfm2  23988  fmfnfmlem1  23994  fmco  24001  fbflim2  24017  flffbas  24035  flftg  24036  cnpflf2  24040  alexsubALTlem4  24090  neibl  24541  metcnp3  24580  xlebnum  25007  lebnumii  25008  caubl  25350  caublcls  25351  bcthlem2  25367  bcthlem5  25370  ovolsslem  25526  volsuplem  25597  dyadmbllem  25641  ellimc3  25921  limciun  25936  cpnord  25977  precsexlem6  28282  precsexlem7  28283  ubthlem1  31019  occon3  31446  chsupval  31484  chsupcl  31489  chsupss  31491  spanss  31497  chsupval2  31559  stlei  32389  dmdbr5  32457  mdsl0  32459  chrelat2i  32514  chirredlem1  32539  mdsymlem5  32556  mdsymlem6  32557  gsumvsca1  33367  gsumvsca2  33368  omsmon  34556  cvmliftlem15  35612  ss2mcls  35882  mclsax  35883  clsint2  36653  fgmin  36694  filnetlem4  36705  limsucncmpi  36769  bj-restpw  37546  bj-0int  37555  rdgssun  37836  ptrecube  38083  heiborlem1  38274  heiborlem8  38281  refrelsredund4  39179  refrelredund4  39182  funALTVss  39247  pclssN  40482  dochexmidlem7  42054  incssnn0  43256  islssfg2  43612  hbtlem6  43670  hess  44320  psshepw  44328  clsf2  44666  mnuunid  44817  ismnushort  44841  sspwimpcf  45459  sspwimpcfVD  45460  dvmptfprod  46483  sprsymrelfo  48067  elbigo2  49138  subthinc  50028  setrec1lem2  50273  setrec1lem4  50275  setrec2mpt  50282