Theorem sstr2 3946

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

Syntax hints:   → wi 4  ∀wal 1561   ∈ wcel 2145   ⊆ wss 3907

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

This theorem depends on definitions:  df-bi 210  df-ss 3924

This theorem is referenced by:  sstr  3947  sstri  3948  sseq1  3964  sseq2  3965  ssun3  4135  ssun4  4136  ssinss1OLD  4201  sspw  4569  triun  5227  trintss  5231  exss  5435  frss  5616  relss  5759  funss  6544  funimass2  6608  fss  6712  limsssuc  7834  oaordi  8519  oeworde  8567  nnaordi  8592  sbthlem2  9064  sbthlem3  9065  sbthlem6  9068  domunfican  9269  fiint  9274  fiss  9372  dffi3  9379  inf3lem1  9585  trcl  9685  tcss  9699  ac10ct  10006  ackbij2lem4  10212  cfslb  10238  cfslbn  10239  cfcoflem  10244  coftr  10245  fin23lem15  10306  fin23lem20  10309  fin23lem36  10320  isf32lem1  10325  axdc3lem2  10423  ttukeylem2  10482  wunex2  10711  tskcard  10754  clsslem  15011  mrcss  17662  isacs2  17699  lubss  18559  frmdss2  18912  lsmlub  19725  gsumle  20206  lsslss  21051  lspss  21074  ocv2ss  21783  ocvsscon  21785  lindsss  21934  lsslinds  21941  aspss  21986  mplcoe1  22148  mplcoe5  22151  mdetunilem9  22738  tgss  23086  tgcl  23087  tgss3  23104  clsss  23172  ntrss  23173  neiss  23227  ssnei2  23234  opnnei  23238  cnpnei  23382  cnpco  23385  cncls  23392  cnprest  23407  hauscmp  23525  1stcfb  23563  1stcelcls  23579  reftr  23632  txcnpi  23726  txcnp  23738  txtube  23758  qtoptop2  23817  fgcl  23996  filssufilg  24029  ufileu  24037  uffix  24039  elfm2  24066  fmfnfmlem1  24072  fmco  24079  fbflim2  24095  flffbas  24113  flftg  24114  cnpflf2  24118  alexsubALTlem4  24168  neibl  24619  metcnp3  24658  xlebnum  25085  lebnumii  25086  caubl  25428  caublcls  25429  bcthlem2  25445  bcthlem5  25448  ovolsslem  25604  volsuplem  25675  dyadmbllem  25719  ellimc3  25999  limciun  26014  cpnord  26055  precsexlem6  28363  precsexlem7  28364  ubthlem1  31131  occon3  31558  chsupval  31596  chsupcl  31601  chsupss  31603  spanss  31609  chsupval2  31671  stlei  32501  dmdbr5  32569  mdsl0  32571  chrelat2i  32626  chirredlem1  32651  mdsymlem5  32668  mdsymlem6  32669  gsumvsca1  33459  gsumvsca2  33460  omsmon  34605  cvmliftlem15  35661  ss2mcls  35931  mclsax  35932  clsint2  36702  fgmin  36743  filnetlem4  36754  limsucncmpi  36818  bj-restpw  37594  bj-0int  37603  rdgssun  37884  ptrecube  38131  heiborlem1  38322  heiborlem8  38329  refrelsredund4  39227  refrelredund4  39230  funALTVss  39295  pclssN  40530  dochexmidlem7  42102  incssnn0  43304  islssfg2  43660  hbtlem6  43718  hess  44368  psshepw  44376  clsf2  44714  mnuunid  44851  ismnushort  44875  sspwimpcf  45493  sspwimpcfVD  45494  dvmptfprod  46517  sprsymrelfo  48101  elbigo2  49183  subthinc  50072  setrec1lem2  50317  setrec1lem4  50319  setrec2mpt  50326