Theorem sstr2 3944

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

Syntax hints:   → wi 4  ∀wal 1538   ∈ wcel 2109   ⊆ wss 3905

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

This theorem depends on definitions:  df-bi 207  df-ss 3922

This theorem is referenced by:  sstr  3946  sstri  3947  sseq1  3963  sseq2  3964  ssun3  4133  ssun4  4134  ssinss1  4199  sspw  4564  triun  5216  trintss  5220  exss  5410  frss  5587  relss  5729  funss  6505  funimass2  6569  fss  6672  sucexeloniOLD  7750  limsssuc  7790  oaordi  8471  oeworde  8518  nnaordi  8543  sbthlem2  9012  sbthlem3  9013  sbthlem6  9016  domunfican  9230  fiint  9235  fiintOLD  9236  fiss  9333  dffi3  9340  inf3lem1  9543  trcl  9643  tcss  9659  ac10ct  9947  ackbij2lem4  10154  cfslb  10179  cfslbn  10180  cfcoflem  10185  coftr  10186  fin23lem15  10247  fin23lem20  10250  fin23lem36  10261  isf32lem1  10266  axdc3lem2  10364  ttukeylem2  10423  wunex2  10651  tskcard  10694  clsslem  14909  mrcss  17540  isacs2  17577  lubss  18437  frmdss2  18755  lsmlub  19561  gsumle  20042  lsslss  20882  lspss  20905  ocv2ss  21598  ocvsscon  21600  lindsss  21749  lsslinds  21756  aspss  21802  mplcoe1  21960  mplcoe5  21963  mdetunilem9  22523  tgss  22871  tgcl  22872  tgss3  22889  clsss  22957  ntrss  22958  neiss  23012  ssnei2  23019  opnnei  23023  cnpnei  23167  cnpco  23170  cncls  23177  cnprest  23192  hauscmp  23310  1stcfb  23348  1stcelcls  23364  reftr  23417  txcnpi  23511  txcnp  23523  txtube  23543  qtoptop2  23602  fgcl  23781  filssufilg  23814  ufileu  23822  uffix  23824  elfm2  23851  fmfnfmlem1  23857  fmco  23864  fbflim2  23880  flffbas  23898  flftg  23899  cnpflf2  23903  alexsubALTlem4  23953  neibl  24405  metcnp3  24444  xlebnum  24880  lebnumii  24881  caubl  25224  caublcls  25225  bcthlem2  25241  bcthlem5  25244  ovolsslem  25401  volsuplem  25472  dyadmbllem  25516  ellimc3  25796  limciun  25811  cpnord  25853  precsexlem6  28137  precsexlem7  28138  ubthlem1  30832  occon3  31259  chsupval  31297  chsupcl  31302  chsupss  31304  spanss  31310  chsupval2  31372  stlei  32202  dmdbr5  32270  mdsl0  32272  chrelat2i  32327  chirredlem1  32352  mdsymlem5  32369  mdsymlem6  32370  gsumvsca1  33178  gsumvsca2  33179  omsmon  34265  cvmliftlem15  35270  ss2mcls  35540  mclsax  35541  clsint2  36302  fgmin  36343  filnetlem4  36354  limsucncmpi  36418  bj-restpw  37065  bj-0int  37074  rdgssun  37351  ptrecube  37599  heiborlem1  37790  heiborlem8  37797  refrelsredund4  38608  refrelredund4  38611  funALTVss  38676  pclssN  39873  dochexmidlem7  41445  incssnn0  42684  islssfg2  43044  hbtlem6  43102  hess  43753  psshepw  43761  clsf2  44099  mnuunid  44250  ismnushort  44274  sspwimpcf  44893  sspwimpcfVD  44894  dvmptfprod  45927  sprsymrelfo  47482  elbigo2  48538  subthinc  49429  setrec1lem2  49674  setrec1lem4  49676  setrec2mpt  49683