Theorem sstr2 3940

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

Syntax hints:   → wi 4  ∀wal 1539   ∈ wcel 2113   ⊆ wss 3901

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 3918

This theorem is referenced by:  sstr  3942  sstri  3943  sseq1  3959  sseq2  3960  ssun3  4132  ssun4  4133  ssinss1  4198  sspw  4565  triun  5219  trintss  5223  exss  5411  frss  5588  relss  5731  funss  6511  funimass2  6575  fss  6678  limsssuc  7792  oaordi  8473  oeworde  8521  nnaordi  8546  sbthlem2  9016  sbthlem3  9017  sbthlem6  9020  domunfican  9222  fiint  9227  fiss  9327  dffi3  9334  inf3lem1  9537  trcl  9637  tcss  9651  ac10ct  9944  ackbij2lem4  10151  cfslb  10176  cfslbn  10177  cfcoflem  10182  coftr  10183  fin23lem15  10244  fin23lem20  10247  fin23lem36  10258  isf32lem1  10263  axdc3lem2  10361  ttukeylem2  10420  wunex2  10649  tskcard  10692  clsslem  14907  mrcss  17539  isacs2  17576  lubss  18436  frmdss2  18788  lsmlub  19593  gsumle  20074  lsslss  20912  lspss  20935  ocv2ss  21628  ocvsscon  21630  lindsss  21779  lsslinds  21786  aspss  21832  mplcoe1  21992  mplcoe5  21995  mdetunilem9  22564  tgss  22912  tgcl  22913  tgss3  22930  clsss  22998  ntrss  22999  neiss  23053  ssnei2  23060  opnnei  23064  cnpnei  23208  cnpco  23211  cncls  23218  cnprest  23233  hauscmp  23351  1stcfb  23389  1stcelcls  23405  reftr  23458  txcnpi  23552  txcnp  23564  txtube  23584  qtoptop2  23643  fgcl  23822  filssufilg  23855  ufileu  23863  uffix  23865  elfm2  23892  fmfnfmlem1  23898  fmco  23905  fbflim2  23921  flffbas  23939  flftg  23940  cnpflf2  23944  alexsubALTlem4  23994  neibl  24445  metcnp3  24484  xlebnum  24920  lebnumii  24921  caubl  25264  caublcls  25265  bcthlem2  25281  bcthlem5  25284  ovolsslem  25441  volsuplem  25512  dyadmbllem  25556  ellimc3  25836  limciun  25851  cpnord  25893  precsexlem6  28208  precsexlem7  28209  ubthlem1  30945  occon3  31372  chsupval  31410  chsupcl  31415  chsupss  31417  spanss  31423  chsupval2  31485  stlei  32315  dmdbr5  32383  mdsl0  32385  chrelat2i  32440  chirredlem1  32465  mdsymlem5  32482  mdsymlem6  32483  gsumvsca1  33308  gsumvsca2  33309  omsmon  34455  cvmliftlem15  35492  ss2mcls  35762  mclsax  35763  clsint2  36523  fgmin  36564  filnetlem4  36575  limsucncmpi  36639  bj-restpw  37293  bj-0int  37302  rdgssun  37579  ptrecube  37817  heiborlem1  38008  heiborlem8  38015  refrelsredund4  38885  refrelredund4  38888  funALTVss  38954  pclssN  40150  dochexmidlem7  41722  incssnn0  42949  islssfg2  43309  hbtlem6  43367  hess  44017  psshepw  44025  clsf2  44363  mnuunid  44514  ismnushort  44538  sspwimpcf  45156  sspwimpcfVD  45157  dvmptfprod  46185  sprsymrelfo  47739  elbigo2  48794  subthinc  49684  setrec1lem2  49929  setrec1lem4  49931  setrec2mpt  49938