Theorem sstr2 3923

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

Syntax hints:   → wi 4  ∀wal 1546   ∈ wcel 2121   ⊆ wss 3884

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

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

This theorem is referenced by:  sstr  3924  sstri  3925  sseq1  3941  sseq2  3942  ssun3  4111  ssun4  4112  ssinss1  4176  sspw  4542  triun  5196  trintss  5200  exss  5404  frss  5584  relss  5727  funss  6507  funimass2  6571  fss  6674  limsssuc  7793  oaordi  8475  oeworde  8523  nnaordi  8548  sbthlem2  9020  sbthlem3  9021  sbthlem6  9024  domunfican  9226  fiint  9231  fiss  9331  dffi3  9338  inf3lem1  9544  trcl  9644  tcss  9658  ac10ct  9951  ackbij2lem4  10158  cfslb  10184  cfslbn  10185  cfcoflem  10190  coftr  10191  fin23lem15  10252  fin23lem20  10255  fin23lem36  10266  isf32lem1  10271  axdc3lem2  10369  ttukeylem2  10428  wunex2  10657  tskcard  10700  clsslem  14941  mrcss  17577  isacs2  17614  lubss  18474  frmdss2  18826  lsmlub  19633  gsumle  20114  lsslss  20954  lspss  20977  ocv2ss  21651  ocvsscon  21653  lindsss  21802  lsslinds  21809  aspss  21854  mplcoe1  22016  mplcoe5  22019  mdetunilem9  22606  tgss  22954  tgcl  22955  tgss3  22972  clsss  23040  ntrss  23041  neiss  23095  ssnei2  23102  opnnei  23106  cnpnei  23250  cnpco  23253  cncls  23260  cnprest  23275  hauscmp  23393  1stcfb  23431  1stcelcls  23447  reftr  23500  txcnpi  23594  txcnp  23606  txtube  23626  qtoptop2  23685  fgcl  23864  filssufilg  23897  ufileu  23905  uffix  23907  elfm2  23934  fmfnfmlem1  23940  fmco  23947  fbflim2  23963  flffbas  23981  flftg  23982  cnpflf2  23986  alexsubALTlem4  24036  neibl  24487  metcnp3  24526  xlebnum  24953  lebnumii  24954  caubl  25296  caublcls  25297  bcthlem2  25313  bcthlem5  25316  ovolsslem  25472  volsuplem  25543  dyadmbllem  25587  ellimc3  25867  limciun  25882  cpnord  25923  precsexlem6  28224  precsexlem7  28225  ubthlem1  30961  occon3  31388  chsupval  31426  chsupcl  31431  chsupss  31433  spanss  31439  chsupval2  31501  stlei  32331  dmdbr5  32399  mdsl0  32401  chrelat2i  32456  chirredlem1  32481  mdsymlem5  32498  mdsymlem6  32499  gsumvsca1  33309  gsumvsca2  33310  omsmon  34492  cvmliftlem15  35539  ss2mcls  35809  mclsax  35810  clsint2  36570  fgmin  36611  filnetlem4  36622  limsucncmpi  36686  bj-restpw  37463  bj-0int  37472  rdgssun  37753  ptrecube  38000  heiborlem1  38191  heiborlem8  38198  refrelsredund4  39096  refrelredund4  39099  funALTVss  39164  pclssN  40399  dochexmidlem7  41971  incssnn0  43173  islssfg2  43529  hbtlem6  43587  hess  44237  psshepw  44245  clsf2  44583  mnuunid  44734  ismnushort  44758  sspwimpcf  45376  sspwimpcfVD  45377  dvmptfprod  46400  sprsymrelfo  47984  elbigo2  49055  subthinc  49945  setrec1lem2  50190  setrec1lem4  50192  setrec2mpt  50199