Theorem sstr2 3956

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

Syntax hints:   → wi 4  ∀wal 1538   ∈ wcel 2109   ⊆ wss 3917

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 3934

This theorem is referenced by:  sstr  3958  sstri  3959  sseq1  3975  sseq2  3976  ssun3  4146  ssun4  4147  ssinss1  4212  sspw  4577  triun  5232  trintss  5236  exss  5426  frss  5605  relss  5747  funss  6538  funimass2  6602  fss  6707  sucexeloniOLD  7789  limsssuc  7829  oaordi  8513  oeworde  8560  nnaordi  8585  sbthlem2  9058  sbthlem3  9059  sbthlem6  9062  domunfican  9279  fiint  9284  fiintOLD  9285  fiss  9382  dffi3  9389  inf3lem1  9588  trcl  9688  tcss  9704  ac10ct  9994  ackbij2lem4  10201  cfslb  10226  cfslbn  10227  cfcoflem  10232  coftr  10233  fin23lem15  10294  fin23lem20  10297  fin23lem36  10308  isf32lem1  10313  axdc3lem2  10411  ttukeylem2  10470  wunex2  10698  tskcard  10741  clsslem  14957  mrcss  17584  isacs2  17621  lubss  18479  frmdss2  18797  lsmlub  19601  lsslss  20874  lspss  20897  ocv2ss  21589  ocvsscon  21591  lindsss  21740  lsslinds  21747  aspss  21793  mplcoe1  21951  mplcoe5  21954  mdetunilem9  22514  tgss  22862  tgcl  22863  tgss3  22880  clsss  22948  ntrss  22949  neiss  23003  ssnei2  23010  opnnei  23014  cnpnei  23158  cnpco  23161  cncls  23168  cnprest  23183  hauscmp  23301  1stcfb  23339  1stcelcls  23355  reftr  23408  txcnpi  23502  txcnp  23514  txtube  23534  qtoptop2  23593  fgcl  23772  filssufilg  23805  ufileu  23813  uffix  23815  elfm2  23842  fmfnfmlem1  23848  fmco  23855  fbflim2  23871  flffbas  23889  flftg  23890  cnpflf2  23894  alexsubALTlem4  23944  neibl  24396  metcnp3  24435  xlebnum  24871  lebnumii  24872  caubl  25215  caublcls  25216  bcthlem2  25232  bcthlem5  25235  ovolsslem  25392  volsuplem  25463  dyadmbllem  25507  ellimc3  25787  limciun  25802  cpnord  25844  precsexlem6  28121  precsexlem7  28122  ubthlem1  30806  occon3  31233  chsupval  31271  chsupcl  31276  chsupss  31278  spanss  31284  chsupval2  31346  stlei  32176  dmdbr5  32244  mdsl0  32246  chrelat2i  32301  chirredlem1  32326  mdsymlem5  32343  mdsymlem6  32344  gsumle  33045  gsumvsca1  33186  gsumvsca2  33187  omsmon  34296  cvmliftlem15  35292  ss2mcls  35562  mclsax  35563  clsint2  36324  fgmin  36365  filnetlem4  36376  limsucncmpi  36440  bj-restpw  37087  bj-0int  37096  rdgssun  37373  ptrecube  37621  heiborlem1  37812  heiborlem8  37819  refrelsredund4  38630  refrelredund4  38633  funALTVss  38698  pclssN  39895  dochexmidlem7  41467  incssnn0  42706  islssfg2  43067  hbtlem6  43125  hess  43776  psshepw  43784  clsf2  44122  mnuunid  44273  ismnushort  44297  sspwimpcf  44916  sspwimpcfVD  44917  dvmptfprod  45950  sprsymrelfo  47502  elbigo2  48545  subthinc  49436  setrec1lem2  49681  setrec1lem4  49683  setrec2mpt  49690