Theorem sstr2 3973

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

Syntax hints:   → wi 4  ∀wal 1531   ∈ wcel 2110   ⊆ wss 3935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3942  df-ss 3951

This theorem is referenced by:  sstr  3974  sstri  3975  sseq1  3991  sseq2  3992  ssun3  4149  ssun4  4150  ssinss1  4213  sspw  4551  triun  5184  trintss  5188  exss  5354  frss  5521  relss  5655  funss  6373  funimass2  6436  fss  6526  suceloni  7527  limsssuc  7564  oaordi  8171  oeworde  8218  nnaordi  8243  sbthlem2  8627  sbthlem3  8628  sbthlem6  8631  domunfican  8790  fiint  8794  fiss  8887  dffi3  8894  inf3lem1  9090  trcl  9169  tcss  9185  ac10ct  9459  ackbij2lem4  9663  cfslb  9687  cfslbn  9688  cfcoflem  9693  coftr  9694  fin23lem15  9755  fin23lem20  9758  fin23lem36  9769  isf32lem1  9774  axdc3lem2  9872  ttukeylem2  9931  wunex2  10159  tskcard  10202  clsslem  14343  mrcss  16886  isacs2  16923  lubss  17730  frmdss2  18027  lsmlub  18789  lsslss  19732  lspss  19755  aspss  20105  mplcoe1  20245  mplcoe5  20248  ocv2ss  20816  ocvsscon  20818  lindsss  20967  lsslinds  20974  mdetunilem9  21228  tgss  21575  tgcl  21576  tgss3  21593  clsss  21661  ntrss  21662  neiss  21716  ssnei2  21723  opnnei  21727  cnpnei  21871  cnpco  21874  cncls  21881  cnprest  21896  hauscmp  22014  1stcfb  22052  1stcelcls  22068  reftr  22121  txcnpi  22215  txcnp  22227  txtube  22247  qtoptop2  22306  fgcl  22485  filssufilg  22518  ufileu  22526  uffix  22528  elfm2  22555  fmfnfmlem1  22561  fmco  22568  fbflim2  22584  flffbas  22602  flftg  22603  cnpflf2  22607  alexsubALTlem4  22657  neibl  23110  metcnp3  23149  xlebnum  23568  lebnumii  23569  caubl  23910  caublcls  23911  bcthlem2  23927  bcthlem5  23930  ovolsslem  24084  volsuplem  24155  dyadmbllem  24199  ellimc3  24476  limciun  24491  cpnord  24531  ubthlem1  28646  occon3  29073  chsupval  29111  chsupcl  29116  chsupss  29118  spanss  29124  chsupval2  29186  stlei  30016  dmdbr5  30084  mdsl0  30086  chrelat2i  30141  chirredlem1  30166  mdsymlem5  30183  mdsymlem6  30184  gsumle  30725  gsumvsca1  30854  gsumvsca2  30855  omsmon  31556  cvmliftlem15  32545  ss2mcls  32815  mclsax  32816  clsint2  33677  fgmin  33718  filnetlem4  33729  limsucncmpi  33793  bj-restpw  34382  bj-0int  34392  rdgssun  34658  ptrecube  34891  heiborlem1  35088  heiborlem8  35095  refrelsredund4  35866  refrelredund4  35869  funALTVss  35931  pclssN  37029  dochexmidlem7  38601  incssnn0  39306  islssfg2  39669  hbtlem6  39727  hess  40124  psshepw  40132  clsf2  40474  mnuunid  40611  sspwimpcf  41252  sspwimpcfVD  41253  dvmptfprod  42228  sprsymrelfo  43658  elbigo2  44611  setrec1lem2  44790  setrec1lem4  44792