Theorem sstr2 3922

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

Syntax hints:   → wi 4  ∀wal 1536   ∈ wcel 2111   ⊆ wss 3881

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898

This theorem is referenced by:  sstr  3923  sstri  3924  sseq1  3940  sseq2  3941  ssun3  4101  ssun4  4102  ssinss1  4164  sspw  4510  triun  5149  trintss  5153  exss  5320  frss  5486  relss  5620  funss  6343  funimass2  6407  fss  6501  suceloni  7508  limsssuc  7545  oaordi  8155  oeworde  8202  nnaordi  8227  sbthlem2  8612  sbthlem3  8613  sbthlem6  8616  domunfican  8775  fiint  8779  fiss  8872  dffi3  8879  inf3lem1  9075  trcl  9154  tcss  9170  ac10ct  9445  ackbij2lem4  9653  cfslb  9677  cfslbn  9678  cfcoflem  9683  coftr  9684  fin23lem15  9745  fin23lem20  9748  fin23lem36  9759  isf32lem1  9764  axdc3lem2  9862  ttukeylem2  9921  wunex2  10149  tskcard  10192  clsslem  14335  mrcss  16879  isacs2  16916  lubss  17723  frmdss2  18020  lsmlub  18782  lsslss  19726  lspss  19749  ocv2ss  20362  ocvsscon  20364  lindsss  20513  lsslinds  20520  aspss  20563  mplcoe1  20705  mplcoe5  20708  mdetunilem9  21225  tgss  21573  tgcl  21574  tgss3  21591  clsss  21659  ntrss  21660  neiss  21714  ssnei2  21721  opnnei  21725  cnpnei  21869  cnpco  21872  cncls  21879  cnprest  21894  hauscmp  22012  1stcfb  22050  1stcelcls  22066  reftr  22119  txcnpi  22213  txcnp  22225  txtube  22245  qtoptop2  22304  fgcl  22483  filssufilg  22516  ufileu  22524  uffix  22526  elfm2  22553  fmfnfmlem1  22559  fmco  22566  fbflim2  22582  flffbas  22600  flftg  22601  cnpflf2  22605  alexsubALTlem4  22655  neibl  23108  metcnp3  23147  xlebnum  23570  lebnumii  23571  caubl  23912  caublcls  23913  bcthlem2  23929  bcthlem5  23932  ovolsslem  24088  volsuplem  24159  dyadmbllem  24203  ellimc3  24482  limciun  24497  cpnord  24538  ubthlem1  28653  occon3  29080  chsupval  29118  chsupcl  29123  chsupss  29125  spanss  29131  chsupval2  29193  stlei  30023  dmdbr5  30091  mdsl0  30093  chrelat2i  30148  chirredlem1  30173  mdsymlem5  30190  mdsymlem6  30191  gsumle  30775  gsumvsca1  30904  gsumvsca2  30905  omsmon  31666  cvmliftlem15  32658  ss2mcls  32928  mclsax  32929  clsint2  33790  fgmin  33831  filnetlem4  33842  limsucncmpi  33906  bj-restpw  34507  bj-0int  34516  rdgssun  34795  ptrecube  35057  heiborlem1  35249  heiborlem8  35256  refrelsredund4  36027  refrelredund4  36030  funALTVss  36092  pclssN  37190  dochexmidlem7  38762  incssnn0  39652  islssfg2  40015  hbtlem6  40073  hess  40481  psshepw  40489  clsf2  40829  mnuunid  40985  sspwimpcf  41626  sspwimpcfVD  41627  dvmptfprod  42587  sprsymrelfo  44014  elbigo2  44966  setrec1lem2  45218  setrec1lem4  45220