Theorem sstr2 3928

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

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

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 3906

This theorem is referenced by:  sstr  3930  sstri  3931  sseq1  3947  sseq2  3948  ssun3  4120  ssun4  4121  ssinss1  4186  sspw  4552  triun  5207  trintss  5211  exss  5415  frss  5595  relss  5738  funss  6517  funimass2  6581  fss  6684  limsssuc  7801  oaordi  8481  oeworde  8529  nnaordi  8554  sbthlem2  9026  sbthlem3  9027  sbthlem6  9030  domunfican  9232  fiint  9237  fiss  9337  dffi3  9344  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  14946  mrcss  17582  isacs2  17619  lubss  18479  frmdss2  18831  lsmlub  19639  gsumle  20120  lsslss  20956  lspss  20979  ocv2ss  21653  ocvsscon  21655  lindsss  21804  lsslinds  21811  aspss  21856  mplcoe1  22015  mplcoe5  22018  mdetunilem9  22585  tgss  22933  tgcl  22934  tgss3  22951  clsss  23019  ntrss  23020  neiss  23074  ssnei2  23081  opnnei  23085  cnpnei  23229  cnpco  23232  cncls  23239  cnprest  23254  hauscmp  23372  1stcfb  23410  1stcelcls  23426  reftr  23479  txcnpi  23573  txcnp  23585  txtube  23605  qtoptop2  23664  fgcl  23843  filssufilg  23876  ufileu  23884  uffix  23886  elfm2  23913  fmfnfmlem1  23919  fmco  23926  fbflim2  23942  flffbas  23960  flftg  23961  cnpflf2  23965  alexsubALTlem4  24015  neibl  24466  metcnp3  24505  xlebnum  24932  lebnumii  24933  caubl  25275  caublcls  25276  bcthlem2  25292  bcthlem5  25295  ovolsslem  25451  volsuplem  25522  dyadmbllem  25566  ellimc3  25846  limciun  25861  cpnord  25902  precsexlem6  28204  precsexlem7  28205  ubthlem1  30941  occon3  31368  chsupval  31406  chsupcl  31411  chsupss  31413  spanss  31419  chsupval2  31481  stlei  32311  dmdbr5  32379  mdsl0  32381  chrelat2i  32436  chirredlem1  32461  mdsymlem5  32478  mdsymlem6  32479  gsumvsca1  33287  gsumvsca2  33288  omsmon  34442  cvmliftlem15  35480  ss2mcls  35750  mclsax  35751  clsint2  36511  fgmin  36552  filnetlem4  36563  limsucncmpi  36627  bj-restpw  37404  bj-0int  37413  rdgssun  37694  ptrecube  37941  heiborlem1  38132  heiborlem8  38139  refrelsredund4  39037  refrelredund4  39040  funALTVss  39105  pclssN  40340  dochexmidlem7  41912  incssnn0  43143  islssfg2  43499  hbtlem6  43557  hess  44207  psshepw  44215  clsf2  44553  mnuunid  44704  ismnushort  44728  sspwimpcf  45346  sspwimpcfVD  45347  dvmptfprod  46373  sprsymrelfo  47957  elbigo2  49028  subthinc  49918  setrec1lem2  50163  setrec1lem4  50165  setrec2mpt  50172