Theorem sstr2 3942

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

Syntax hints:   → wi 4  ∀wal 1540   ∈ wcel 2114   ⊆ wss 3903

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

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

This theorem is referenced by:  sstr  3944  sstri  3945  sseq1  3961  sseq2  3962  ssun3  4134  ssun4  4135  ssinss1  4200  sspw  4567  triun  5221  trintss  5225  exss  5418  frss  5596  relss  5739  funss  6519  funimass2  6583  fss  6686  limsssuc  7802  oaordi  8483  oeworde  8531  nnaordi  8556  sbthlem2  9028  sbthlem3  9029  sbthlem6  9032  domunfican  9234  fiint  9239  fiss  9339  dffi3  9346  inf3lem1  9549  trcl  9649  tcss  9663  ac10ct  9956  ackbij2lem4  10163  cfslb  10188  cfslbn  10189  cfcoflem  10194  coftr  10195  fin23lem15  10256  fin23lem20  10259  fin23lem36  10270  isf32lem1  10275  axdc3lem2  10373  ttukeylem2  10432  wunex2  10661  tskcard  10704  clsslem  14919  mrcss  17551  isacs2  17588  lubss  18448  frmdss2  18800  lsmlub  19605  gsumle  20086  lsslss  20924  lspss  20947  ocv2ss  21640  ocvsscon  21642  lindsss  21791  lsslinds  21798  aspss  21844  mplcoe1  22004  mplcoe5  22007  mdetunilem9  22576  tgss  22924  tgcl  22925  tgss3  22942  clsss  23010  ntrss  23011  neiss  23065  ssnei2  23072  opnnei  23076  cnpnei  23220  cnpco  23223  cncls  23230  cnprest  23245  hauscmp  23363  1stcfb  23401  1stcelcls  23417  reftr  23470  txcnpi  23564  txcnp  23576  txtube  23596  qtoptop2  23655  fgcl  23834  filssufilg  23867  ufileu  23875  uffix  23877  elfm2  23904  fmfnfmlem1  23910  fmco  23917  fbflim2  23933  flffbas  23951  flftg  23952  cnpflf2  23956  alexsubALTlem4  24006  neibl  24457  metcnp3  24496  xlebnum  24932  lebnumii  24933  caubl  25276  caublcls  25277  bcthlem2  25293  bcthlem5  25296  ovolsslem  25453  volsuplem  25524  dyadmbllem  25568  ellimc3  25848  limciun  25863  cpnord  25905  precsexlem6  28220  precsexlem7  28221  ubthlem1  30957  occon3  31384  chsupval  31422  chsupcl  31427  chsupss  31429  spanss  31435  chsupval2  31497  stlei  32327  dmdbr5  32395  mdsl0  32397  chrelat2i  32452  chirredlem1  32477  mdsymlem5  32494  mdsymlem6  32495  gsumvsca1  33319  gsumvsca2  33320  omsmon  34475  cvmliftlem15  35511  ss2mcls  35781  mclsax  35782  clsint2  36542  fgmin  36583  filnetlem4  36594  limsucncmpi  36658  bj-restpw  37339  bj-0int  37348  rdgssun  37627  ptrecube  37865  heiborlem1  38056  heiborlem8  38063  refrelsredund4  38961  refrelredund4  38964  funALTVss  39029  pclssN  40264  dochexmidlem7  41836  incssnn0  43062  islssfg2  43422  hbtlem6  43480  hess  44130  psshepw  44138  clsf2  44476  mnuunid  44627  ismnushort  44651  sspwimpcf  45269  sspwimpcfVD  45270  dvmptfprod  46297  sprsymrelfo  47851  elbigo2  48906  subthinc  49796  setrec1lem2  50041  setrec1lem4  50043  setrec2mpt  50050