Theorem sstr2 3924

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

Syntax hints:   → wi 4  ∀wal 1537   ∈ wcel 2108   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  sstr  3925  sstri  3926  sseq1  3942  sseq2  3943  ssun3  4104  ssun4  4105  ssinss1  4168  sspw  4543  triun  5200  trintss  5204  exss  5372  frss  5547  relss  5682  funss  6437  funimass2  6501  fss  6601  suceloni  7635  limsssuc  7672  oaordi  8339  oeworde  8386  nnaordi  8411  sbthlem2  8824  sbthlem3  8825  sbthlem6  8828  domunfican  9017  fiint  9021  fiss  9113  dffi3  9120  inf3lem1  9316  trcl  9417  tcss  9433  ac10ct  9721  ackbij2lem4  9929  cfslb  9953  cfslbn  9954  cfcoflem  9959  coftr  9960  fin23lem15  10021  fin23lem20  10024  fin23lem36  10035  isf32lem1  10040  axdc3lem2  10138  ttukeylem2  10197  wunex2  10425  tskcard  10468  clsslem  14623  mrcss  17242  isacs2  17279  lubss  18146  frmdss2  18417  lsmlub  19185  lsslss  20138  lspss  20161  ocv2ss  20790  ocvsscon  20792  lindsss  20941  lsslinds  20948  aspss  20991  mplcoe1  21148  mplcoe5  21151  mdetunilem9  21677  tgss  22026  tgcl  22027  tgss3  22044  clsss  22113  ntrss  22114  neiss  22168  ssnei2  22175  opnnei  22179  cnpnei  22323  cnpco  22326  cncls  22333  cnprest  22348  hauscmp  22466  1stcfb  22504  1stcelcls  22520  reftr  22573  txcnpi  22667  txcnp  22679  txtube  22699  qtoptop2  22758  fgcl  22937  filssufilg  22970  ufileu  22978  uffix  22980  elfm2  23007  fmfnfmlem1  23013  fmco  23020  fbflim2  23036  flffbas  23054  flftg  23055  cnpflf2  23059  alexsubALTlem4  23109  neibl  23563  metcnp3  23602  xlebnum  24034  lebnumii  24035  caubl  24377  caublcls  24378  bcthlem2  24394  bcthlem5  24397  ovolsslem  24553  volsuplem  24624  dyadmbllem  24668  ellimc3  24948  limciun  24963  cpnord  25004  ubthlem1  29133  occon3  29560  chsupval  29598  chsupcl  29603  chsupss  29605  spanss  29611  chsupval2  29673  stlei  30503  dmdbr5  30571  mdsl0  30573  chrelat2i  30628  chirredlem1  30653  mdsymlem5  30670  mdsymlem6  30671  gsumle  31252  gsumvsca1  31381  gsumvsca2  31382  omsmon  32165  cvmliftlem15  33160  ss2mcls  33430  mclsax  33431  clsint2  34445  fgmin  34486  filnetlem4  34497  limsucncmpi  34561  bj-restpw  35190  bj-0int  35199  rdgssun  35476  ptrecube  35704  heiborlem1  35896  heiborlem8  35903  refrelsredund4  36672  refrelredund4  36675  funALTVss  36737  pclssN  37835  dochexmidlem7  39407  incssnn0  40449  islssfg2  40812  hbtlem6  40870  hess  41277  psshepw  41285  clsf2  41625  mnuunid  41784  ismnushort  41808  sspwimpcf  42429  sspwimpcfVD  42430  dvmptfprod  43376  sprsymrelfo  44837  elbigo2  45786  subthinc  46209  setrec1lem2  46280  setrec1lem4  46282