Theorem sstr2 3990

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.)

Assertion

Ref	Expression
sstr2	⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶))

Proof of Theorem sstr2

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ssel 3976	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2	1	imim1d 82	. . 3 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)))
3	2	alimdv 1920	. 2 ⊢ (𝐴 ⊆ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶) → ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)))
4		dfss2 3969	. 2 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶))
5		dfss2 3969	. 2 ⊢ (𝐴 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶))
6	3, 4, 5	3imtr4g 296	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶))

Syntax hints:   → wi 4  ∀wal 1540   ∈ wcel 2107   ⊆ wss 3949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966

This theorem is referenced by:  sstr  3991  sstri  3992  sseq1  4008  sseq2  4009  ssun3  4175  ssun4  4176  ssinss1  4238  sspw  4614  triun  5281  trintss  5285  exss  5464  frss  5644  relss  5782  funss  6568  funimass2  6632  fss  6735  sucexeloniOLD  7798  suceloniOLD  7800  limsssuc  7839  oaordi  8546  oeworde  8593  nnaordi  8618  sbthlem2  9084  sbthlem3  9085  sbthlem6  9088  domunfican  9320  fiint  9324  fiss  9419  dffi3  9426  inf3lem1  9623  trcl  9723  tcss  9739  ac10ct  10029  ackbij2lem4  10237  cfslb  10261  cfslbn  10262  cfcoflem  10267  coftr  10268  fin23lem15  10329  fin23lem20  10332  fin23lem36  10343  isf32lem1  10348  axdc3lem2  10446  ttukeylem2  10505  wunex2  10733  tskcard  10776  clsslem  14931  mrcss  17560  isacs2  17597  lubss  18466  frmdss2  18744  lsmlub  19532  lsslss  20572  lspss  20595  ocv2ss  21226  ocvsscon  21228  lindsss  21379  lsslinds  21386  aspss  21431  mplcoe1  21592  mplcoe5  21595  mdetunilem9  22122  tgss  22471  tgcl  22472  tgss3  22489  clsss  22558  ntrss  22559  neiss  22613  ssnei2  22620  opnnei  22624  cnpnei  22768  cnpco  22771  cncls  22778  cnprest  22793  hauscmp  22911  1stcfb  22949  1stcelcls  22965  reftr  23018  txcnpi  23112  txcnp  23124  txtube  23144  qtoptop2  23203  fgcl  23382  filssufilg  23415  ufileu  23423  uffix  23425  elfm2  23452  fmfnfmlem1  23458  fmco  23465  fbflim2  23481  flffbas  23499  flftg  23500  cnpflf2  23504  alexsubALTlem4  23554  neibl  24010  metcnp3  24049  xlebnum  24481  lebnumii  24482  caubl  24825  caublcls  24826  bcthlem2  24842  bcthlem5  24845  ovolsslem  25001  volsuplem  25072  dyadmbllem  25116  ellimc3  25396  limciun  25411  cpnord  25452  precsexlem6  27658  precsexlem7  27659  ubthlem1  30123  occon3  30550  chsupval  30588  chsupcl  30593  chsupss  30595  spanss  30601  chsupval2  30663  stlei  31493  dmdbr5  31561  mdsl0  31563  chrelat2i  31618  chirredlem1  31643  mdsymlem5  31660  mdsymlem6  31661  gsumle  32242  gsumvsca1  32371  gsumvsca2  32372  omsmon  33297  cvmliftlem15  34289  ss2mcls  34559  mclsax  34560  clsint2  35214  fgmin  35255  filnetlem4  35266  limsucncmpi  35330  bj-restpw  35973  bj-0int  35982  rdgssun  36259  ptrecube  36488  heiborlem1  36679  heiborlem8  36686  refrelsredund4  37502  refrelredund4  37505  funALTVss  37569  pclssN  38765  dochexmidlem7  40337  incssnn0  41449  islssfg2  41813  hbtlem6  41871  hess  42531  psshepw  42539  clsf2  42877  mnuunid  43036  ismnushort  43060  sspwimpcf  43681  sspwimpcfVD  43682  dvmptfprod  44661  sprsymrelfo  46165  elbigo2  47238  subthinc  47660  setrec1lem2  47733  setrec1lem4  47735  setrec2mpt  47742