Theorem sstr2 4001

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

Syntax hints:   → wi 4  ∀wal 1534   ∈ wcel 2105   ⊆ wss 3962

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

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

This theorem is referenced by:  sstr  4003  sstri  4004  sseq1  4020  sseq2  4021  ssun3  4189  ssun4  4190  ssinss1  4253  sspw  4615  triun  5279  trintss  5283  exss  5473  frss  5652  relss  5793  funss  6586  funimass2  6650  fss  6752  sucexeloniOLD  7829  suceloniOLD  7831  limsssuc  7870  oaordi  8582  oeworde  8629  nnaordi  8654  sbthlem2  9122  sbthlem3  9123  sbthlem6  9126  domunfican  9358  fiint  9363  fiintOLD  9364  fiss  9461  dffi3  9468  inf3lem1  9665  trcl  9765  tcss  9781  ac10ct  10071  ackbij2lem4  10278  cfslb  10303  cfslbn  10304  cfcoflem  10309  coftr  10310  fin23lem15  10371  fin23lem20  10374  fin23lem36  10385  isf32lem1  10390  axdc3lem2  10488  ttukeylem2  10547  wunex2  10775  tskcard  10818  clsslem  15019  mrcss  17660  isacs2  17697  lubss  18570  frmdss2  18888  lsmlub  19696  lsslss  20976  lspss  20999  ocv2ss  21708  ocvsscon  21710  lindsss  21861  lsslinds  21868  aspss  21914  mplcoe1  22072  mplcoe5  22075  mdetunilem9  22641  tgss  22990  tgcl  22991  tgss3  23008  clsss  23077  ntrss  23078  neiss  23132  ssnei2  23139  opnnei  23143  cnpnei  23287  cnpco  23290  cncls  23297  cnprest  23312  hauscmp  23430  1stcfb  23468  1stcelcls  23484  reftr  23537  txcnpi  23631  txcnp  23643  txtube  23663  qtoptop2  23722  fgcl  23901  filssufilg  23934  ufileu  23942  uffix  23944  elfm2  23971  fmfnfmlem1  23977  fmco  23984  fbflim2  24000  flffbas  24018  flftg  24019  cnpflf2  24023  alexsubALTlem4  24073  neibl  24529  metcnp3  24568  xlebnum  25010  lebnumii  25011  caubl  25355  caublcls  25356  bcthlem2  25372  bcthlem5  25375  ovolsslem  25532  volsuplem  25603  dyadmbllem  25647  ellimc3  25928  limciun  25943  cpnord  25985  precsexlem6  28250  precsexlem7  28251  ubthlem1  30898  occon3  31325  chsupval  31363  chsupcl  31368  chsupss  31370  spanss  31376  chsupval2  31438  stlei  32268  dmdbr5  32336  mdsl0  32338  chrelat2i  32393  chirredlem1  32418  mdsymlem5  32435  mdsymlem6  32436  gsumle  33083  gsumvsca1  33214  gsumvsca2  33215  omsmon  34279  cvmliftlem15  35282  ss2mcls  35552  mclsax  35553  clsint2  36311  fgmin  36352  filnetlem4  36363  limsucncmpi  36427  bj-restpw  37074  bj-0int  37083  rdgssun  37360  ptrecube  37606  heiborlem1  37797  heiborlem8  37804  refrelsredund4  38613  refrelredund4  38616  funALTVss  38680  pclssN  39876  dochexmidlem7  41448  incssnn0  42698  islssfg2  43059  hbtlem6  43117  hess  43769  psshepw  43777  clsf2  44115  mnuunid  44272  ismnushort  44296  sspwimpcf  44917  sspwimpcfVD  44918  dvmptfprod  45900  sprsymrelfo  47421  elbigo2  48401  subthinc  48839  setrec1lem2  48918  setrec1lem4  48920  setrec2mpt  48927