Theorem sstr2 3938

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1568   ∈ wcel 2145   ⊆ wss 3899

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

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

This theorem is used by:  sstr  3939  sstri  3940  sseq1  3956  sseq2  3957  ssun3  4126  ssun4  4127  ssinss1OLD  4192  sspw  4568  triun  5227  trintss  5231  exss  5431  frss  5615  relss  5758  funss  6550  funimass2  6615  fss  6718  limsssuc  7850  oaordi  8538  oeworde  8586  nnaordi  8611  sbthlem2  9091  sbthlem3  9092  sbthlem6  9095  domunfican  9297  fiint  9302  fiss  9400  dffi3  9407  inf3lem1  9613  trcl  9713  tcss  9727  setrec1lem2  9948  setrec1lem4  9952  ackbij2lem4  10300  cfslb  10325  cfslbn  10326  cfcoflem  10331  coftr  10332  fin23lem15  10393  fin23lem20  10396  fin23lem36  10407  isf32lem1  10412  axdc3lem2  10510  ttukeylem2  10569  wunex2  10804  tskcard  10847  clsslem  15117  mrcss  17770  isacs2  17807  lubss  18667  frmdss2  19039  lsmlub  19858  gsumle  20339  lsslss  21216  lspss  21239  ocv2ss  21959  ocvsscon  21961  lindsss  22110  lsslinds  22117  aspss  22164  mplcoe1  22326  mplcoe5  22329  mdetunilem9  22915  tgss  23266  tgcl  23267  tgss3  23284  clsss  23352  ntrss  23353  neiss  23407  ssnei2  23414  opnnei  23418  cnpnei  23562  cnpco  23565  cncls  23572  cnprest  23587  hauscmp  23705  1stcfb  23743  1stcelcls  23760  reftr  23813  txcnpi  23907  txcnp  23919  txtube  23939  qtoptop2  23998  fgcl  24177  filssufilg  24210  ufileu  24218  uffix  24220  elfm2  24247  fmfnfmlem1  24253  fmco  24260  fbflim2  24276  flffbas  24294  flftg  24295  cnpflf2  24299  alexsubALTlem4  24349  neibl  24800  metcnp3  24839  xlebnum  25266  lebnumii  25267  caubl  25609  caublcls  25610  bcthlem2  25626  bcthlem5  25629  ovolsslem  25785  volsuplem  25856  dyadmbllem  25900  ellimc3  26179  limciun  26194  cpnord  26235  precsexlem6  28580  precsexlem7  28581  ubthlem1  31454  occon3  31881  chsupval  31919  chsupcl  31924  chsupss  31926  spanss  31932  chsupval2  31994  stlei  32824  dmdbr5  32892  mdsl0  32894  chrelat2i  32949  chirredlem1  32974  mdsymlem5  32991  mdsymlem6  32992  gsumvsca1  33769  gsumvsca2  33770  omsmon  34913  cvmliftlem15  36032  ss2mcls  36302  mclsax  36303  clsint2  37087  fgmin  37128  filnetlem4  37139  limsucncmpi  37203  bj-restpw  37981  bj-0int  37990  rdgssun  38269  ptrecube  38506  dfprop2  38614  heiborlem1  38713  heiborlem8  38720  refrelsredund4  39616  refrelredund4  39619  funALTVss  39684  pclssN  40919  dochexmidlem7  42491  incssnn0  43675  islssfg2  44031  hbtlem6  44089  hess  44739  psshepw  44747  clsf2  45085  mnuunid  45220  ismnushort  45244  sspwimpcf  45861  sspwimpcfVD  45862  dvmptfprod  46899  sprsymrelfo  48523  elbigo2  49608  subthinc  50495  setrec2mpt  50734