Theorem sstr2 3953

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

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

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 3931

This theorem is referenced by:  sstr  3955  sstri  3956  sseq1  3972  sseq2  3973  ssun3  4143  ssun4  4144  ssinss1  4209  sspw  4574  triun  5229  trintss  5233  exss  5423  frss  5602  relss  5744  funss  6535  funimass2  6599  fss  6704  sucexeloniOLD  7786  limsssuc  7826  oaordi  8510  oeworde  8557  nnaordi  8582  sbthlem2  9052  sbthlem3  9053  sbthlem6  9056  domunfican  9272  fiint  9277  fiintOLD  9278  fiss  9375  dffi3  9382  inf3lem1  9581  trcl  9681  tcss  9697  ac10ct  9987  ackbij2lem4  10194  cfslb  10219  cfslbn  10220  cfcoflem  10225  coftr  10226  fin23lem15  10287  fin23lem20  10290  fin23lem36  10301  isf32lem1  10306  axdc3lem2  10404  ttukeylem2  10463  wunex2  10691  tskcard  10734  clsslem  14950  mrcss  17577  isacs2  17614  lubss  18472  frmdss2  18790  lsmlub  19594  lsslss  20867  lspss  20890  ocv2ss  21582  ocvsscon  21584  lindsss  21733  lsslinds  21740  aspss  21786  mplcoe1  21944  mplcoe5  21947  mdetunilem9  22507  tgss  22855  tgcl  22856  tgss3  22873  clsss  22941  ntrss  22942  neiss  22996  ssnei2  23003  opnnei  23007  cnpnei  23151  cnpco  23154  cncls  23161  cnprest  23176  hauscmp  23294  1stcfb  23332  1stcelcls  23348  reftr  23401  txcnpi  23495  txcnp  23507  txtube  23527  qtoptop2  23586  fgcl  23765  filssufilg  23798  ufileu  23806  uffix  23808  elfm2  23835  fmfnfmlem1  23841  fmco  23848  fbflim2  23864  flffbas  23882  flftg  23883  cnpflf2  23887  alexsubALTlem4  23937  neibl  24389  metcnp3  24428  xlebnum  24864  lebnumii  24865  caubl  25208  caublcls  25209  bcthlem2  25225  bcthlem5  25228  ovolsslem  25385  volsuplem  25456  dyadmbllem  25500  ellimc3  25780  limciun  25795  cpnord  25837  precsexlem6  28114  precsexlem7  28115  ubthlem1  30799  occon3  31226  chsupval  31264  chsupcl  31269  chsupss  31271  spanss  31277  chsupval2  31339  stlei  32169  dmdbr5  32237  mdsl0  32239  chrelat2i  32294  chirredlem1  32319  mdsymlem5  32336  mdsymlem6  32337  gsumle  33038  gsumvsca1  33179  gsumvsca2  33180  omsmon  34289  cvmliftlem15  35285  ss2mcls  35555  mclsax  35556  clsint2  36317  fgmin  36358  filnetlem4  36369  limsucncmpi  36433  bj-restpw  37080  bj-0int  37089  rdgssun  37366  ptrecube  37614  heiborlem1  37805  heiborlem8  37812  refrelsredund4  38623  refrelredund4  38626  funALTVss  38691  pclssN  39888  dochexmidlem7  41460  incssnn0  42699  islssfg2  43060  hbtlem6  43118  hess  43769  psshepw  43777  clsf2  44115  mnuunid  44266  ismnushort  44290  sspwimpcf  44909  sspwimpcfVD  44910  dvmptfprod  45943  sprsymrelfo  47498  elbigo2  48541  subthinc  49432  setrec1lem2  49677  setrec1lem4  49679  setrec2mpt  49686