Theorem sstr2 3805

Description: Transitivity of subclasses. 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 3792	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2	1	imim1d 82	. . 3 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)))
3	2	alimdv 2007	. 2 ⊢ (𝐴 ⊆ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶) → ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)))
4		dfss2 3786	. 2 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶))
5		dfss2 3786	. 2 ⊢ (𝐴 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶))
6	3, 4, 5	3imtr4g 287	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶))

Syntax hints:   → wi 4  ∀wal 1635   ∈ wcel 2156   ⊆ wss 3769

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-ext 2784

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-in 3776  df-ss 3783

This theorem is referenced by:  sstr  3806  sstri  3807  sseq1  3823  sseq2  3824  ssun3  3977  ssun4  3978  ssinss1  4038  triun  4959  trintss  4962  sspwb  5107  exss  5121  frss  5278  relss  5408  funss  6120  funimass2  6183  fss  6269  suceloni  7243  limsssuc  7280  oaordi  7863  oeworde  7910  nnaordi  7935  sbthlem2  8310  sbthlem3  8311  sbthlem6  8314  domunfican  8472  fiint  8476  fiss  8569  dffi3  8576  inf3lem1  8772  trcl  8851  tcss  8867  ac10ct  9140  ackbij2lem4  9349  cfslb  9373  cfslbn  9374  cfcoflem  9379  coftr  9380  fin23lem15  9441  fin23lem20  9444  fin23lem36  9455  isf32lem1  9460  axdc3lem2  9558  ttukeylem2  9617  wunex2  9845  tskcard  9888  clsslem  13948  mrcss  16481  isacs2  16518  lubss  17326  frmdss2  17605  lsmlub  18279  lsslss  19168  lspss  19191  aspss  19541  mplcoe1  19674  mplcoe5  19677  ocv2ss  20227  ocvsscon  20229  lindsss  20373  lsslinds  20380  mdetunilem9  20637  tgss  20986  tgcl  20987  tgss3  21004  clsss  21072  ntrss  21073  neiss  21127  ssnei2  21134  opnnei  21138  cnpnei  21282  cnpco  21285  cncls  21292  cnprest  21307  hauscmp  21424  1stcfb  21462  1stcelcls  21478  reftr  21531  txcnpi  21625  txcnp  21637  txtube  21657  qtoptop2  21716  fgcl  21895  filssufilg  21928  ufileu  21936  uffix  21938  elfm2  21965  fmfnfmlem1  21971  fmco  21978  fbflim2  21994  flffbas  22012  flftg  22013  cnpflf2  22017  alexsubALTlem4  22067  neibl  22519  metcnp3  22558  xlebnum  22977  lebnumii  22978  caubl  23318  caublcls  23319  bcthlem2  23334  bcthlem5  23337  ovolsslem  23465  volsuplem  23536  dyadmbllem  23580  ellimc3  23857  limciun  23872  cpnord  23912  ubthlem1  28054  occon3  28484  chsupval  28522  chsupcl  28527  chsupss  28529  spanss  28535  chsupval2  28597  stlei  29427  dmdbr5  29495  mdsl0  29497  chrelat2i  29552  chirredlem1  29577  mdsymlem5  29594  mdsymlem6  29595  gsumle  30104  gsumvsca1  30107  gsumvsca2  30108  omsmon  30685  cvmliftlem15  31603  ss2mcls  31788  mclsax  31789  clsint2  32645  fgmin  32686  filnetlem4  32697  limsucncmpi  32761  bj-restpw  33356  bj-0int  33366  ptrecube  33722  heiborlem1  33921  heiborlem8  33928  pclssN  35674  dochexmidlem7  37247  incssnn0  37776  islssfg2  38142  hbtlem6  38200  hess  38574  psshepw  38582  clsf2  38924  sspwimpcf  39650  sspwimpcfVD  39651  dvmptfprod  40640  sprsymrelfo  42315  elbigo2  42914  setrec1lem2  43003  setrec1lem4  43005