Theorem sstr2 3861

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

Syntax hints:   → wi 4  ∀wal 1505   ∈ wcel 2048   ⊆ wss 3825

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-ext 2745

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-clab 2754  df-cleq 2765  df-clel 2840  df-in 3832  df-ss 3839

This theorem is referenced by:  sstr  3862  sstri  3863  sseq1  3878  sseq2  3879  ssun3  4035  ssun4  4036  ssinss1  4096  triun  5037  trintss  5042  sspwb  5191  exss  5205  frss  5367  relss  5499  funss  6201  funimass2  6264  fss  6351  suceloni  7338  limsssuc  7375  oaordi  7965  oeworde  8012  nnaordi  8037  sbthlem2  8416  sbthlem3  8417  sbthlem6  8420  domunfican  8578  fiint  8582  fiss  8675  dffi3  8682  inf3lem1  8877  trcl  8956  tcss  8972  ac10ct  9246  ackbij2lem4  9454  cfslb  9478  cfslbn  9479  cfcoflem  9484  coftr  9485  fin23lem15  9546  fin23lem20  9549  fin23lem36  9560  isf32lem1  9565  axdc3lem2  9663  ttukeylem2  9722  wunex2  9950  tskcard  9993  clsslem  14195  mrcss  16735  isacs2  16772  lubss  17579  frmdss2  17859  lsmlub  18539  lsslss  19445  lspss  19468  aspss  19816  mplcoe1  19949  mplcoe5  19952  ocv2ss  20509  ocvsscon  20511  lindsss  20660  lsslinds  20667  mdetunilem9  20923  tgss  21270  tgcl  21271  tgss3  21288  clsss  21356  ntrss  21357  neiss  21411  ssnei2  21418  opnnei  21422  cnpnei  21566  cnpco  21569  cncls  21576  cnprest  21591  hauscmp  21709  1stcfb  21747  1stcelcls  21763  reftr  21816  txcnpi  21910  txcnp  21922  txtube  21942  qtoptop2  22001  fgcl  22180  filssufilg  22213  ufileu  22221  uffix  22223  elfm2  22250  fmfnfmlem1  22256  fmco  22263  fbflim2  22279  flffbas  22297  flftg  22298  cnpflf2  22302  alexsubALTlem4  22352  neibl  22804  metcnp3  22843  xlebnum  23262  lebnumii  23263  caubl  23604  caublcls  23605  bcthlem2  23621  bcthlem5  23624  ovolsslem  23778  volsuplem  23849  dyadmbllem  23893  ellimc3  24170  limciun  24185  cpnord  24225  ubthlem1  28415  occon3  28845  chsupval  28883  chsupcl  28888  chsupss  28890  spanss  28896  chsupval2  28958  stlei  29788  dmdbr5  29856  mdsl0  29858  chrelat2i  29913  chirredlem1  29938  mdsymlem5  29955  mdsymlem6  29956  gsumle  30478  gsumvsca1  30481  gsumvsca2  30482  omsmon  31158  cvmliftlem15  32090  ss2mcls  32275  mclsax  32276  clsint2  33138  fgmin  33179  filnetlem4  33190  limsucncmpi  33253  bj-restpw  33828  bj-0int  33838  rdgssun  34036  ptrecube  34281  heiborlem1  34479  heiborlem8  34486  refrelsredund4  35260  refrelredund4  35263  funALTVss  35325  pclssN  36423  dochexmidlem7  37995  incssnn0  38648  islssfg2  39012  hbtlem6  39070  hess  39434  psshepw  39442  clsf2  39784  mnuunid  39933  sspwimpcf  40617  sspwimpcfVD  40618  dvmptfprod  41606  sprsymrelfo  42967  elbigo2  43920  setrec1lem2  44098  setrec1lem4  44100