Theorem sstr2 3941

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

Syntax hints:   → wi 4  ∀wal 1539   ∈ wcel 2111   ⊆ wss 3902

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

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

This theorem is referenced by:  sstr  3943  sstri  3944  sseq1  3960  sseq2  3961  ssun3  4130  ssun4  4131  ssinss1  4196  sspw  4561  triun  5212  trintss  5216  exss  5403  frss  5580  relss  5722  funss  6500  funimass2  6564  fss  6667  limsssuc  7780  oaordi  8461  oeworde  8508  nnaordi  8533  sbthlem2  9001  sbthlem3  9002  sbthlem6  9005  domunfican  9206  fiint  9211  fiss  9308  dffi3  9315  inf3lem1  9518  trcl  9618  tcss  9634  ac10ct  9922  ackbij2lem4  10129  cfslb  10154  cfslbn  10155  cfcoflem  10160  coftr  10161  fin23lem15  10222  fin23lem20  10225  fin23lem36  10236  isf32lem1  10241  axdc3lem2  10339  ttukeylem2  10398  wunex2  10626  tskcard  10669  clsslem  14888  mrcss  17519  isacs2  17556  lubss  18416  frmdss2  18768  lsmlub  19574  gsumle  20055  lsslss  20892  lspss  20915  ocv2ss  21608  ocvsscon  21610  lindsss  21759  lsslinds  21766  aspss  21812  mplcoe1  21970  mplcoe5  21973  mdetunilem9  22533  tgss  22881  tgcl  22882  tgss3  22899  clsss  22967  ntrss  22968  neiss  23022  ssnei2  23029  opnnei  23033  cnpnei  23177  cnpco  23180  cncls  23187  cnprest  23202  hauscmp  23320  1stcfb  23358  1stcelcls  23374  reftr  23427  txcnpi  23521  txcnp  23533  txtube  23553  qtoptop2  23612  fgcl  23791  filssufilg  23824  ufileu  23832  uffix  23834  elfm2  23861  fmfnfmlem1  23867  fmco  23874  fbflim2  23890  flffbas  23908  flftg  23909  cnpflf2  23913  alexsubALTlem4  23963  neibl  24414  metcnp3  24453  xlebnum  24889  lebnumii  24890  caubl  25233  caublcls  25234  bcthlem2  25250  bcthlem5  25253  ovolsslem  25410  volsuplem  25481  dyadmbllem  25525  ellimc3  25805  limciun  25820  cpnord  25862  precsexlem6  28148  precsexlem7  28149  ubthlem1  30845  occon3  31272  chsupval  31310  chsupcl  31315  chsupss  31317  spanss  31323  chsupval2  31385  stlei  32215  dmdbr5  32283  mdsl0  32285  chrelat2i  32340  chirredlem1  32365  mdsymlem5  32382  mdsymlem6  32383  gsumvsca1  33190  gsumvsca2  33191  omsmon  34306  cvmliftlem15  35330  ss2mcls  35600  mclsax  35601  clsint2  36362  fgmin  36403  filnetlem4  36414  limsucncmpi  36478  bj-restpw  37125  bj-0int  37134  rdgssun  37411  ptrecube  37659  heiborlem1  37850  heiborlem8  37857  refrelsredund4  38668  refrelredund4  38671  funALTVss  38736  pclssN  39932  dochexmidlem7  41504  incssnn0  42743  islssfg2  43103  hbtlem6  43161  hess  43812  psshepw  43820  clsf2  44158  mnuunid  44309  ismnushort  44333  sspwimpcf  44951  sspwimpcfVD  44952  dvmptfprod  45982  sprsymrelfo  47527  elbigo2  48583  subthinc  49474  setrec1lem2  49719  setrec1lem4  49721  setrec2mpt  49728