Theorem sstr2 3988

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 3974	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2	1	imim1d 82	. . 3 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)))
3	2	alimdv 1919	. 2 ⊢ (𝐴 ⊆ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶) → ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)))
4		dfss2 3967	. 2 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶))
5		dfss2 3967	. 2 ⊢ (𝐴 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶))
6	3, 4, 5	3imtr4g 295	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶))

Syntax hints:   → wi 4  ∀wal 1539   ∈ wcel 2106   ⊆ wss 3947

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3954  df-ss 3964

This theorem is referenced by:  sstr  3989  sstri  3990  sseq1  4006  sseq2  4007  ssun3  4173  ssun4  4174  ssinss1  4236  sspw  4612  triun  5279  trintss  5283  exss  5462  frss  5642  relss  5779  funss  6564  funimass2  6628  fss  6731  sucexeloniOLD  7794  suceloniOLD  7796  limsssuc  7835  oaordi  8542  oeworde  8589  nnaordi  8614  sbthlem2  9080  sbthlem3  9081  sbthlem6  9084  domunfican  9316  fiint  9320  fiss  9415  dffi3  9422  inf3lem1  9619  trcl  9719  tcss  9735  ac10ct  10025  ackbij2lem4  10233  cfslb  10257  cfslbn  10258  cfcoflem  10263  coftr  10264  fin23lem15  10325  fin23lem20  10328  fin23lem36  10339  isf32lem1  10344  axdc3lem2  10442  ttukeylem2  10501  wunex2  10729  tskcard  10772  clsslem  14927  mrcss  17556  isacs2  17593  lubss  18462  frmdss2  18740  lsmlub  19526  lsslss  20564  lspss  20587  ocv2ss  21217  ocvsscon  21219  lindsss  21370  lsslinds  21377  aspss  21422  mplcoe1  21583  mplcoe5  21586  mdetunilem9  22113  tgss  22462  tgcl  22463  tgss3  22480  clsss  22549  ntrss  22550  neiss  22604  ssnei2  22611  opnnei  22615  cnpnei  22759  cnpco  22762  cncls  22769  cnprest  22784  hauscmp  22902  1stcfb  22940  1stcelcls  22956  reftr  23009  txcnpi  23103  txcnp  23115  txtube  23135  qtoptop2  23194  fgcl  23373  filssufilg  23406  ufileu  23414  uffix  23416  elfm2  23443  fmfnfmlem1  23449  fmco  23456  fbflim2  23472  flffbas  23490  flftg  23491  cnpflf2  23495  alexsubALTlem4  23545  neibl  24001  metcnp3  24040  xlebnum  24472  lebnumii  24473  caubl  24816  caublcls  24817  bcthlem2  24833  bcthlem5  24836  ovolsslem  24992  volsuplem  25063  dyadmbllem  25107  ellimc3  25387  limciun  25402  cpnord  25443  precsexlem6  27647  precsexlem7  27648  ubthlem1  30110  occon3  30537  chsupval  30575  chsupcl  30580  chsupss  30582  spanss  30588  chsupval2  30650  stlei  31480  dmdbr5  31548  mdsl0  31550  chrelat2i  31605  chirredlem1  31630  mdsymlem5  31647  mdsymlem6  31648  gsumle  32229  gsumvsca1  32358  gsumvsca2  32359  omsmon  33285  cvmliftlem15  34277  ss2mcls  34547  mclsax  34548  clsint2  35202  fgmin  35243  filnetlem4  35254  limsucncmpi  35318  bj-restpw  35961  bj-0int  35970  rdgssun  36247  ptrecube  36476  heiborlem1  36667  heiborlem8  36674  refrelsredund4  37490  refrelredund4  37493  funALTVss  37557  pclssN  38753  dochexmidlem7  40325  incssnn0  41434  islssfg2  41798  hbtlem6  41856  hess  42516  psshepw  42524  clsf2  42862  mnuunid  43021  ismnushort  43045  sspwimpcf  43666  sspwimpcfVD  43667  dvmptfprod  44647  sprsymrelfo  46151  elbigo2  47191  subthinc  47613  setrec1lem2  47686  setrec1lem4  47688  setrec2mpt  47695