Theorem sstr2 3965

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

Syntax hints:   → wi 4  ∀wal 1538   ∈ wcel 2108   ⊆ wss 3926

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 3943

This theorem is referenced by:  sstr  3967  sstri  3968  sseq1  3984  sseq2  3985  ssun3  4155  ssun4  4156  ssinss1  4221  sspw  4586  triun  5244  trintss  5248  exss  5438  frss  5618  relss  5760  funss  6554  funimass2  6618  fss  6721  sucexeloniOLD  7802  suceloniOLD  7804  limsssuc  7843  oaordi  8556  oeworde  8603  nnaordi  8628  sbthlem2  9096  sbthlem3  9097  sbthlem6  9100  domunfican  9331  fiint  9336  fiintOLD  9337  fiss  9434  dffi3  9441  inf3lem1  9640  trcl  9740  tcss  9756  ac10ct  10046  ackbij2lem4  10253  cfslb  10278  cfslbn  10279  cfcoflem  10284  coftr  10285  fin23lem15  10346  fin23lem20  10349  fin23lem36  10360  isf32lem1  10365  axdc3lem2  10463  ttukeylem2  10522  wunex2  10750  tskcard  10793  clsslem  15001  mrcss  17626  isacs2  17663  lubss  18521  frmdss2  18839  lsmlub  19643  lsslss  20916  lspss  20939  ocv2ss  21631  ocvsscon  21633  lindsss  21782  lsslinds  21789  aspss  21835  mplcoe1  21993  mplcoe5  21996  mdetunilem9  22556  tgss  22904  tgcl  22905  tgss3  22922  clsss  22990  ntrss  22991  neiss  23045  ssnei2  23052  opnnei  23056  cnpnei  23200  cnpco  23203  cncls  23210  cnprest  23225  hauscmp  23343  1stcfb  23381  1stcelcls  23397  reftr  23450  txcnpi  23544  txcnp  23556  txtube  23576  qtoptop2  23635  fgcl  23814  filssufilg  23847  ufileu  23855  uffix  23857  elfm2  23884  fmfnfmlem1  23890  fmco  23897  fbflim2  23913  flffbas  23931  flftg  23932  cnpflf2  23936  alexsubALTlem4  23986  neibl  24438  metcnp3  24477  xlebnum  24913  lebnumii  24914  caubl  25258  caublcls  25259  bcthlem2  25275  bcthlem5  25278  ovolsslem  25435  volsuplem  25506  dyadmbllem  25550  ellimc3  25830  limciun  25845  cpnord  25887  precsexlem6  28153  precsexlem7  28154  ubthlem1  30797  occon3  31224  chsupval  31262  chsupcl  31267  chsupss  31269  spanss  31275  chsupval2  31337  stlei  32167  dmdbr5  32235  mdsl0  32237  chrelat2i  32292  chirredlem1  32317  mdsymlem5  32334  mdsymlem6  32335  gsumle  33038  gsumvsca1  33169  gsumvsca2  33170  omsmon  34276  cvmliftlem15  35266  ss2mcls  35536  mclsax  35537  clsint2  36293  fgmin  36334  filnetlem4  36345  limsucncmpi  36409  bj-restpw  37056  bj-0int  37065  rdgssun  37342  ptrecube  37590  heiborlem1  37781  heiborlem8  37788  refrelsredund4  38596  refrelredund4  38599  funALTVss  38663  pclssN  39859  dochexmidlem7  41431  incssnn0  42681  islssfg2  43042  hbtlem6  43100  hess  43751  psshepw  43759  clsf2  44097  mnuunid  44249  ismnushort  44273  sspwimpcf  44892  sspwimpcfVD  44893  dvmptfprod  45922  sprsymrelfo  47459  elbigo2  48480  subthinc  49277  setrec1lem2  49500  setrec1lem4  49502  setrec2mpt  49509