Theorem sstr2 3575

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 3562	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2	1	imim1d 80	. . 3 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)))
3	2	alimdv 1832	. 2 ⊢ (𝐴 ⊆ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶) → ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)))
4		dfss2 3557	. 2 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶))
5		dfss2 3557	. 2 ⊢ (𝐴 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶))
6	3, 4, 5	3imtr4g 284	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶))

Syntax hints:   → wi 4  ∀wal 1473   ∈ wcel 1977   ⊆ wss 3540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554

This theorem is referenced by:  sstr  3576  sstri  3577  sseq1  3589  sseq2  3590  ssun3  3740  ssun4  3741  ssinss1  3803  ssdisjOLD  3979  triun  4694  trint0  4698  sspwb  4844  exss  4858  frss  5005  relss  5129  funss  5822  funimass2  5886  fss  5969  suceloni  6905  limsssuc  6942  oaordi  7513  oeworde  7560  nnaordi  7585  sbthlem2  7956  sbthlem3  7957  sbthlem6  7960  domunfican  8118  fiint  8122  fiss  8213  dffi3  8220  inf3lem1  8408  trcl  8487  tcss  8503  ac10ct  8740  ackbij2lem4  8947  cfslb  8971  cfslbn  8972  cfcoflem  8977  coftr  8978  fin23lem15  9039  fin23lem20  9042  fin23lem36  9053  isf32lem1  9058  axdc3lem2  9156  ttukeylem2  9215  wunex2  9439  tskcard  9482  clsslem  13571  mrcss  16099  isacs2  16137  lubss  16944  frmdss2  17223  lsmlub  17901  lsslss  18782  lspss  18805  aspss  19153  mplcoe1  19286  mplcoe5  19289  ocv2ss  19836  ocvsscon  19838  lindsss  19982  lsslinds  19989  mdetunilem9  20245  tgss  20583  tgcl  20584  tgss3  20601  clsss  20668  ntrss  20669  neiss  20723  ssnei2  20730  opnnei  20734  cnpnei  20878  cnpco  20881  cncls  20888  cnprest  20903  hauscmp  21020  1stcfb  21058  1stcelcls  21074  reftr  21127  txcnpi  21221  txcnp  21233  txtube  21253  qtoptop2  21312  fgcl  21492  filssufilg  21525  ufileu  21533  uffix  21535  elfm2  21562  fmfnfmlem1  21568  fmco  21575  fbflim2  21591  flffbas  21609  flftg  21610  cnpflf2  21614  alexsubALTlem4  21664  neibl  22116  metcnp3  22155  xlebnum  22572  lebnumii  22573  caubl  22914  caublcls  22915  bcthlem2  22930  bcthlem5  22933  ovolsslem  23059  volsuplem  23130  dyadmbllem  23173  ellimc3  23449  limciun  23464  cpnord  23504  ubthlem1  27110  occon3  27540  chsupval  27578  chsupcl  27583  chsupss  27585  spanss  27591  chsupval2  27653  stlei  28483  dmdbr5  28551  mdsl0  28553  chrelat2i  28608  chirredlem1  28633  mdsymlem5  28650  mdsymlem6  28651  gsumle  29110  gsumvsca1  29113  gsumvsca2  29114  omsmon  29687  cvmliftlem15  30534  ss2mcls  30719  mclsax  30720  clsint2  31494  fgmin  31535  filnetlem4  31546  limsucncmpi  31614  bj-restpw  32226  ptrecube  32579  heiborlem1  32780  heiborlem8  32787  pclssN  34198  dochexmidlem7  35773  incssnn0  36292  islssfg2  36659  hbtlem6  36718  hess  37094  psshepw  37102  clsf2  37444  sspwimpcf  38178  sspwimpcfVD  38179  dvmptfprod  38835  elbigo2  42144  setrec1lem2  42234  setrec1lem4  42236