Theorem 3sstr4d 4000

Description: Substitution of equality into both sides of a subclass relationship. (Contributed by NM, 30-Nov-1995.) (Proof shortened by Eric Schmidt, 26-Jan-2007.)

Hypotheses

Ref	Expression
3sstr4d.1	⊢ (𝜑 → 𝐴 ⊆ 𝐵)
3sstr4d.2	⊢ (𝜑 → 𝐶 = 𝐴)
3sstr4d.3	⊢ (𝜑 → 𝐷 = 𝐵)

Assertion

Ref	Expression
3sstr4d	⊢ (𝜑 → 𝐶 ⊆ 𝐷)

Proof of Theorem 3sstr4d

Step	Hyp	Ref	Expression
1		3sstr4d.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐴)
2		3sstr4d.1	. . 3 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
3	1, 2	eqsstrd 3979	. 2 ⊢ (𝜑 → 𝐶 ⊆ 𝐵)
4		3sstr4d.3	. 2 ⊢ (𝜑 → 𝐷 = 𝐵)
5	3, 4	sseqtrrd 3982	1 ⊢ (𝜑 → 𝐶 ⊆ 𝐷)

Syntax hints:   → wi 4   = wceq 1567   ⊆ wss 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-ss 3930

This theorem is referenced by:  rescnvimafod  7066  suppimacnvss  8165  suppimacnv  8166  ressuppss  8175  suppun  8176  ressuppssdif  8177  suppfnss  8181  suppssov1  8189  suppssov2  8190  suppssfv  8194  omwordri  8553  oewordri  8574  oaabs2  8631  naddssim  8668  fiss  9380  harword  9521  fin1a2lem12  10391  fzoss1  13711  fzoss2  13712  ccatdmss  14615  swrd0  14692  cshimadifsn  14862  trclfvss  15039  trclfvcotrg  15049  relexpnnrn  15078  vdwlem6  17042  vdwlem8  17044  hashbcss  17060  mrcss  17668  chnrev  18679  mndpsuppss  18819  snsymgefmndeq  19461  gsumzf1o  19978  gsumzaddlem  19987  dprdres  20096  dprdz  20098  dprdf1o  20100  rngchomfval  20703  rngccofval  20707  rnghmsscmap2  20710  rnghmsscmap  20711  ringchomfval  20732  ringccofval  20736  rhmsscmap2  20739  rhmsscmap  20740  rhmsscrnghm  20746  rngcresringcat  20750  srhmsubc  20761  rhmsubclem3  20768  fldhmsubc  20862  mptscmfsupp0  21022  lspss  21079  lspsntrim  21193  aspss  21991  resspsrbas  22088  resspsradd  22089  resspsrmul  22090  clsss  23176  ntrss  23177  sslm  23421  1stcfb  23567  txss12  23727  prdstopn  23750  imasncls  23814  fmss  24068  flfssfcf  24160  cnpfcfi  24162  ressprdsds  24493  metss2lem  24633  metustto  24675  pi1addval  25172  pi1xfrcnv  25181  equivcau  25424  rrxmvallem  25528  uniiccvol  25704  dyaddisjlem  25719  volsup2  25729  itg2monolem1  25874  itg2gt0  25884  plyss  26321  lgamucov  27164  madess  28021  oldss  28025  addbday  28173  ifpsnprss  29909  wlkp1lem7  29964  occon  31576  spanss  31637  shlej1  31649  chscllem1  31926  chscllem2  31927  chscllem3  31928  ofrn2  32922  resf1o  33012  fpwrelmap  33015  fldgenss  33576  orvclteinc  34807  dstfrvclim1  34809  reprss  34945  reprinfz1  34950  rankval4b  35432  revwlk  35512  ss2mcls  35955  heiborlem6  38350  lpssat  39672  lssat  39675  paddass  40497  pclssN  40553  2polssN  40574  polcon3N  40576  paddunN  40586  dibss  41828  dicssdvh  41845  dih2dimb  41903  dih2dimbALTN  41904  dihord5b  41918  dochss  42024  dochspss  42037  dvh3dim3N  42108  lclkrlem2r  42183  lclkr  42192  lclkrs  42198  hgmaprnlem2N  42556  hbtlem4  43738  hbtlem3  43739  itgoss  43775  omabs2  43944  naddgeoa  44006  naddwordnexlem4  44013  trrelind  44276  trrelsuperreldg  44279  trrelsuperrel2dg  44282  relexpss1d  44316  trclrelexplem  44322  relexpaddss  44329  frege97d  44363  frege109d  44368  frege131d  44375  clsk1indlem3  44654  limclner  46250  fourierdlem49  46754  fourierdlem92  46797  ovolval5lem3  47253  rhmsubcALTVlem4  48931  srhmsubcALTV  48972  fldhmsubcALTV  48980  rmsuppss  49028  scmsuppss  49029  imassc  49809  setrecsss  50357