Theorem sstr2 3928

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

Syntax hints:   → wi 4  ∀wal 1537   ∈ wcel 2106   ⊆ wss 3887

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904

This theorem is referenced by:  sstr  3929  sstri  3930  sseq1  3946  sseq2  3947  ssun3  4108  ssun4  4109  ssinss1  4171  sspw  4546  triun  5204  trintss  5208  exss  5378  frss  5556  relss  5692  funss  6453  funimass2  6517  fss  6617  sucexeloni  7658  suceloniOLD  7660  limsssuc  7697  oaordi  8377  oeworde  8424  nnaordi  8449  sbthlem2  8871  sbthlem3  8872  sbthlem6  8875  domunfican  9087  fiint  9091  fiss  9183  dffi3  9190  inf3lem1  9386  trcl  9486  tcss  9502  ac10ct  9790  ackbij2lem4  9998  cfslb  10022  cfslbn  10023  cfcoflem  10028  coftr  10029  fin23lem15  10090  fin23lem20  10093  fin23lem36  10104  isf32lem1  10109  axdc3lem2  10207  ttukeylem2  10266  wunex2  10494  tskcard  10537  clsslem  14695  mrcss  17325  isacs2  17362  lubss  18231  frmdss2  18502  lsmlub  19270  lsslss  20223  lspss  20246  ocv2ss  20878  ocvsscon  20880  lindsss  21031  lsslinds  21038  aspss  21081  mplcoe1  21238  mplcoe5  21241  mdetunilem9  21769  tgss  22118  tgcl  22119  tgss3  22136  clsss  22205  ntrss  22206  neiss  22260  ssnei2  22267  opnnei  22271  cnpnei  22415  cnpco  22418  cncls  22425  cnprest  22440  hauscmp  22558  1stcfb  22596  1stcelcls  22612  reftr  22665  txcnpi  22759  txcnp  22771  txtube  22791  qtoptop2  22850  fgcl  23029  filssufilg  23062  ufileu  23070  uffix  23072  elfm2  23099  fmfnfmlem1  23105  fmco  23112  fbflim2  23128  flffbas  23146  flftg  23147  cnpflf2  23151  alexsubALTlem4  23201  neibl  23657  metcnp3  23696  xlebnum  24128  lebnumii  24129  caubl  24472  caublcls  24473  bcthlem2  24489  bcthlem5  24492  ovolsslem  24648  volsuplem  24719  dyadmbllem  24763  ellimc3  25043  limciun  25058  cpnord  25099  ubthlem1  29232  occon3  29659  chsupval  29697  chsupcl  29702  chsupss  29704  spanss  29710  chsupval2  29772  stlei  30602  dmdbr5  30670  mdsl0  30672  chrelat2i  30727  chirredlem1  30752  mdsymlem5  30769  mdsymlem6  30770  gsumle  31350  gsumvsca1  31479  gsumvsca2  31480  omsmon  32265  cvmliftlem15  33260  ss2mcls  33530  mclsax  33531  clsint2  34518  fgmin  34559  filnetlem4  34570  limsucncmpi  34634  bj-restpw  35263  bj-0int  35272  rdgssun  35549  ptrecube  35777  heiborlem1  35969  heiborlem8  35976  refrelsredund4  36745  refrelredund4  36748  funALTVss  36810  pclssN  37908  dochexmidlem7  39480  incssnn0  40533  islssfg2  40896  hbtlem6  40954  hess  41388  psshepw  41396  clsf2  41736  mnuunid  41895  ismnushort  41919  sspwimpcf  42540  sspwimpcfVD  42541  dvmptfprod  43486  sprsymrelfo  44949  elbigo2  45898  subthinc  46321  setrec1lem2  46394  setrec1lem4  46396