Theorem sstr2 3988

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

Syntax hints:   → wi 4  ∀wal 1537   ∈ wcel 2104   ⊆ wss 3947

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-in 3954  df-ss 3964

This theorem is referenced by:  sstr  3989  sstri  3990  sseq1  4006  sseq2  4007  ssun3  4173  ssun4  4174  ssinss1  4236  sspw  4612  triun  5279  trintss  5283  exss  5462  frss  5642  relss  5780  funss  6566  funimass2  6630  fss  6733  sucexeloniOLD  7800  suceloniOLD  7802  limsssuc  7841  oaordi  8548  oeworde  8595  nnaordi  8620  sbthlem2  9086  sbthlem3  9087  sbthlem6  9090  domunfican  9322  fiint  9326  fiss  9421  dffi3  9428  inf3lem1  9625  trcl  9725  tcss  9741  ac10ct  10031  ackbij2lem4  10239  cfslb  10263  cfslbn  10264  cfcoflem  10269  coftr  10270  fin23lem15  10331  fin23lem20  10334  fin23lem36  10345  isf32lem1  10350  axdc3lem2  10448  ttukeylem2  10507  wunex2  10735  tskcard  10778  clsslem  14935  mrcss  17564  isacs2  17601  lubss  18470  frmdss2  18780  lsmlub  19573  lsslss  20716  lspss  20739  ocv2ss  21445  ocvsscon  21447  lindsss  21598  lsslinds  21605  aspss  21650  mplcoe1  21811  mplcoe5  21814  mdetunilem9  22342  tgss  22691  tgcl  22692  tgss3  22709  clsss  22778  ntrss  22779  neiss  22833  ssnei2  22840  opnnei  22844  cnpnei  22988  cnpco  22991  cncls  22998  cnprest  23013  hauscmp  23131  1stcfb  23169  1stcelcls  23185  reftr  23238  txcnpi  23332  txcnp  23344  txtube  23364  qtoptop2  23423  fgcl  23602  filssufilg  23635  ufileu  23643  uffix  23645  elfm2  23672  fmfnfmlem1  23678  fmco  23685  fbflim2  23701  flffbas  23719  flftg  23720  cnpflf2  23724  alexsubALTlem4  23774  neibl  24230  metcnp3  24269  xlebnum  24711  lebnumii  24712  caubl  25056  caublcls  25057  bcthlem2  25073  bcthlem5  25076  ovolsslem  25233  volsuplem  25304  dyadmbllem  25348  ellimc3  25628  limciun  25643  cpnord  25685  precsexlem6  27897  precsexlem7  27898  ubthlem1  30390  occon3  30817  chsupval  30855  chsupcl  30860  chsupss  30862  spanss  30868  chsupval2  30930  stlei  31760  dmdbr5  31828  mdsl0  31830  chrelat2i  31885  chirredlem1  31910  mdsymlem5  31927  mdsymlem6  31928  gsumle  32512  gsumvsca1  32641  gsumvsca2  32642  omsmon  33595  cvmliftlem15  34587  ss2mcls  34857  mclsax  34858  clsint2  35517  fgmin  35558  filnetlem4  35569  limsucncmpi  35633  bj-restpw  36276  bj-0int  36285  rdgssun  36562  ptrecube  36791  heiborlem1  36982  heiborlem8  36989  refrelsredund4  37805  refrelredund4  37808  funALTVss  37872  pclssN  39068  dochexmidlem7  40640  incssnn0  41751  islssfg2  42115  hbtlem6  42173  hess  42833  psshepw  42841  clsf2  43179  mnuunid  43338  ismnushort  43362  sspwimpcf  43983  sspwimpcfVD  43984  dvmptfprod  44959  sprsymrelfo  46463  elbigo2  47325  subthinc  47747  setrec1lem2  47820  setrec1lem4  47822  setrec2mpt  47829