Theorem sstr2 3933

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

Syntax hints:   → wi 4  ∀wal 1540   ∈ wcel 2110   ⊆ wss 3892

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1545  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-v 3433  df-in 3899  df-ss 3909

This theorem is referenced by:  sstr  3934  sstri  3935  sseq1  3951  sseq2  3952  ssun3  4113  ssun4  4114  ssinss1  4177  sspw  4552  triun  5209  trintss  5213  exss  5382  frss  5557  relss  5692  funss  6451  funimass2  6515  fss  6615  sucexeloni  7653  suceloniOLD  7655  limsssuc  7692  oaordi  8369  oeworde  8416  nnaordi  8441  sbthlem2  8862  sbthlem3  8863  sbthlem6  8866  domunfican  9075  fiint  9079  fiss  9171  dffi3  9178  inf3lem1  9374  trcl  9496  tcss  9512  ac10ct  9801  ackbij2lem4  10009  cfslb  10033  cfslbn  10034  cfcoflem  10039  coftr  10040  fin23lem15  10101  fin23lem20  10104  fin23lem36  10115  isf32lem1  10120  axdc3lem2  10218  ttukeylem2  10277  wunex2  10505  tskcard  10548  clsslem  14706  mrcss  17336  isacs2  17373  lubss  18242  frmdss2  18513  lsmlub  19281  lsslss  20234  lspss  20257  ocv2ss  20889  ocvsscon  20891  lindsss  21042  lsslinds  21049  aspss  21092  mplcoe1  21249  mplcoe5  21252  mdetunilem9  21780  tgss  22129  tgcl  22130  tgss3  22147  clsss  22216  ntrss  22217  neiss  22271  ssnei2  22278  opnnei  22282  cnpnei  22426  cnpco  22429  cncls  22436  cnprest  22451  hauscmp  22569  1stcfb  22607  1stcelcls  22623  reftr  22676  txcnpi  22770  txcnp  22782  txtube  22802  qtoptop2  22861  fgcl  23040  filssufilg  23073  ufileu  23081  uffix  23083  elfm2  23110  fmfnfmlem1  23116  fmco  23123  fbflim2  23139  flffbas  23157  flftg  23158  cnpflf2  23162  alexsubALTlem4  23212  neibl  23668  metcnp3  23707  xlebnum  24139  lebnumii  24140  caubl  24483  caublcls  24484  bcthlem2  24500  bcthlem5  24503  ovolsslem  24659  volsuplem  24730  dyadmbllem  24774  ellimc3  25054  limciun  25069  cpnord  25110  ubthlem1  29241  occon3  29668  chsupval  29706  chsupcl  29711  chsupss  29713  spanss  29719  chsupval2  29781  stlei  30611  dmdbr5  30679  mdsl0  30681  chrelat2i  30736  chirredlem1  30761  mdsymlem5  30778  mdsymlem6  30779  gsumle  31359  gsumvsca1  31488  gsumvsca2  31489  omsmon  32274  cvmliftlem15  33269  ss2mcls  33539  mclsax  33540  clsint2  34527  fgmin  34568  filnetlem4  34579  limsucncmpi  34643  bj-restpw  35272  bj-0int  35281  rdgssun  35558  ptrecube  35786  heiborlem1  35978  heiborlem8  35985  refrelsredund4  36754  refrelredund4  36757  funALTVss  36819  pclssN  37917  dochexmidlem7  39489  incssnn0  40542  islssfg2  40905  hbtlem6  40963  hess  41370  psshepw  41378  clsf2  41718  mnuunid  41877  ismnushort  41901  sspwimpcf  42522  sspwimpcfVD  42523  dvmptfprod  43468  sprsymrelfo  44928  elbigo2  45877  subthinc  46300  setrec1lem2  46373  setrec1lem4  46375