Theorem sstr2 3920

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 3901	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
4		df-ss 3901	. . 3 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶))
5		df-ss 3901	. . 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 2147   ⊆ wss 3900

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 3901

This theorem is used by:  sstr  3921  sstri  3922  sseq1  3938  sseq2  3939  ssinss1OLD  4146  ssun3  4181  ssun4  4182  sspw  4571  triun  5231  trintss  5235  exss  5436  frss  5620  relss  5764  funss  6581  funimass2  6648  fss  6751  limsssuc  7888  oaordi  8585  oeworde  8633  nnaordi  8658  sbthlem2  9138  sbthlem3  9139  sbthlem6  9142  domunfican  9344  fiint  9349  fiss  9446  dffi3  9453  inf3lem1  9659  trcl  9759  tcss  9773  setrec1lem2  9997  setrec1lem4  10001  ackbij2lem4  10349  cfslb  10374  cfslbn  10375  cfcoflem  10380  coftr  10381  fin23lem15  10442  fin23lem20  10445  fin23lem36  10456  isf32lem1  10461  axdc3lem2  10559  ttukeylem2  10618  wunex2  10853  tskcard  10896  clsslem  15169  mrcss  17822  isacs2  17859  lubss  18719  frmdss2  19091  lsmlub  19911  gsumle  20392  lsslss  21269  lspss  21292  ocv2ss  22012  ocvsscon  22014  lindsss  22163  lsslinds  22170  aspss  22217  mplcoe1  22379  mplcoe5  22382  mdetunilem9  22968  tgss  23319  tgcl  23320  tgss3  23337  clsss  23405  ntrss  23406  neiss  23460  ssnei2  23467  opnnei  23471  cnpnei  23615  cnpco  23618  cncls  23625  cnprest  23640  hauscmp  23758  1stcfb  23796  1stcelcls  23813  reftr  23866  txcnpi  23960  txcnp  23972  txtube  23992  qtoptop2  24051  fgcl  24230  filssufilg  24263  ufileu  24271  uffix  24273  elfm2  24300  fmfnfmlem1  24306  fmco  24313  fbflim2  24329  flffbas  24347  flftg  24348  cnpflf2  24352  alexsubALTlem4  24402  neibl  24853  metcnp3  24892  xlebnum  25319  lebnumii  25320  caubl  25662  caublcls  25663  bcthlem2  25679  bcthlem5  25682  ovolsslem  25838  volsuplem  25909  dyadmbllem  25953  ellimc3  26232  limciun  26247  cpnord  26288  precsexlem6  28631  precsexlem7  28632  ubthlem1  31505  occon3  31932  chsupval  31970  chsupcl  31975  chsupss  31977  spanss  31983  chsupval2  32045  stlei  32875  dmdbr5  32943  mdsl0  32945  chrelat2i  33000  chirredlem1  33025  mdsymlem5  33042  mdsymlem6  33043  gsumvsca1  33863  gsumvsca2  33864  omsmon  35013  cvmliftlem15  36243  ss2mcls  36513  mclsax  36514  clsint2  37308  fgmin  37349  filnetlem4  37360  limsucncmpi  37424  bj-restpw  38217  bj-0int  38226  rdgssun  38506  ptrecube  38743  dfprop2  38851  heiborlem1  38948  heiborlem8  38955  refrelsredund4  39851  refrelredund4  39854  funALTVss  39919  pclssN  41154  dochexmidlem7  42726  incssnn0  43926  islssfg2  44277  hbtlem6  44334  hess  44983  psshepw  44991  clsf2  45329  mnuunid  45464  ismnushort  45488  sspwimpcf  46104  sspwimpcfVD  46105  dvmptfprod  47170  sprsymrelfo  48794  elbigo2  49879  subthinc  50793  setrec2mpt  51080