Theorem sstr2 3915

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 84	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)))
2	1	al2imi 1847	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) → (∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶) → ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)))
3		df-ss 3896	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
4		df-ss 3896	. . 3 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶))
5		df-ss 3896	. . 3 ⊢ (𝐴 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶))
6	4, 5	imbi12i 353	. 2 ⊢ ((𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶) ↔ (∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶) → ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)))
7	2, 3, 6	3imtr4i 295	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶))

This proof depends on syntax axioms:   → wi 4  ∀wal 1567   ∈ wcel 2144   ⊆ wss 3895

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841

This proof depends on definitions:  df-bi 210  df-ss 3896

This theorem is used by:  sstr  3916  sstri  3917  sseq1  3933  sseq2  3934  ssinss1OLD  4143  ssun3  4178  ssun4  4179  sspw  4567  triun  5226  trintss  5230  exss  5430  frss  5614  relss  5757  funss  6558  funimass2  6623  fss  6726  limsssuc  7861  oaordi  8557  oeworde  8605  nnaordi  8630  sbthlem2  9110  sbthlem3  9111  sbthlem6  9114  domunfican  9316  fiint  9321  fiss  9419  dffi3  9426  inf3lem1  9632  trcl  9732  tcss  9746  setrec1lem2  9970  setrec1lem4  9974  ackbij2lem4  10322  cfslb  10347  cfslbn  10348  cfcoflem  10353  coftr  10354  fin23lem15  10415  fin23lem20  10418  fin23lem36  10429  isf32lem1  10434  axdc3lem2  10532  ttukeylem2  10591  wunex2  10826  tskcard  10869  clsslem  15142  mrcss  17795  isacs2  17832  lubss  18692  frmdss2  19064  lsmlub  19883  gsumle  20364  lsslss  21241  lspss  21264  ocv2ss  21984  ocvsscon  21986  lindsss  22135  lsslinds  22142  aspss  22189  mplcoe1  22351  mplcoe5  22354  mdetunilem9  22940  tgss  23291  tgcl  23292  tgss3  23309  clsss  23377  ntrss  23378  neiss  23432  ssnei2  23439  opnnei  23443  cnpnei  23587  cnpco  23590  cncls  23597  cnprest  23612  hauscmp  23730  1stcfb  23768  1stcelcls  23785  reftr  23838  txcnpi  23932  txcnp  23944  txtube  23964  qtoptop2  24023  fgcl  24202  filssufilg  24235  ufileu  24243  uffix  24245  elfm2  24272  fmfnfmlem1  24278  fmco  24285  fbflim2  24301  flffbas  24319  flftg  24320  cnpflf2  24324  alexsubALTlem4  24374  neibl  24825  metcnp3  24864  xlebnum  25291  lebnumii  25292  caubl  25634  caublcls  25635  bcthlem2  25651  bcthlem5  25654  ovolsslem  25810  volsuplem  25881  dyadmbllem  25925  ellimc3  26204  limciun  26219  cpnord  26260  precsexlem6  28603  precsexlem7  28604  ubthlem1  31477  occon3  31904  chsupval  31942  chsupcl  31947  chsupss  31949  spanss  31955  chsupval2  32017  stlei  32847  dmdbr5  32915  mdsl0  32917  chrelat2i  32972  chirredlem1  32997  mdsymlem5  33014  mdsymlem6  33015  gsumvsca1  33833  gsumvsca2  33834  omsmon  34976  cvmliftlem15  36149  ss2mcls  36419  mclsax  36420  clsint2  37209  fgmin  37250  filnetlem4  37261  limsucncmpi  37325  bj-restpw  38105  bj-0int  38114  rdgssun  38394  ptrecube  38631  dfprop2  38739  heiborlem1  38838  heiborlem8  38845  refrelsredund4  39741  refrelredund4  39744  funALTVss  39809  pclssN  41044  dochexmidlem7  42616  incssnn0  43815  islssfg2  44166  hbtlem6  44224  hess  44873  psshepw  44881  clsf2  45219  mnuunid  45354  ismnushort  45378  sspwimpcf  45995  sspwimpcfVD  45996  dvmptfprod  47048  sprsymrelfo  48672  elbigo2  49757  subthinc  50671  setrec2mpt  50958