Theorem 3sstr4d 4002

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 3981	. 2 ⊢ (𝜑 → 𝐶 ⊆ 𝐵)
4		3sstr4d.3	. 2 ⊢ (𝜑 → 𝐷 = 𝐵)
5	3, 4	sseqtrrd 3984	1 ⊢ (𝜑 → 𝐶 ⊆ 𝐷)

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3914

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 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3931

This theorem is referenced by:  rescnvimafod  7045  suppimacnvss  8152  suppimacnv  8153  ressuppss  8162  suppun  8163  ressuppssdif  8164  suppfnss  8168  suppssov1  8176  suppssov2  8177  suppssfv  8181  omwordri  8536  oewordri  8556  oaabs2  8613  naddssim  8649  fiss  9375  harword  9516  fin1a2lem12  10364  fzoss1  13647  fzoss2  13648  swrd0  14623  cshimadifsn  14795  trclfvss  14972  trclfvcotrg  14982  relexpnnrn  15011  vdwlem6  16957  vdwlem8  16959  hashbcss  16975  mrcss  17577  mndpsuppss  18692  snsymgefmndeq  19325  gsumzf1o  19842  gsumzaddlem  19851  dprdres  19960  dprdz  19962  dprdf1o  19964  rngchomfval  20531  rngccofval  20535  rnghmsscmap2  20538  rnghmsscmap  20539  ringchomfval  20560  ringccofval  20564  rhmsscmap2  20567  rhmsscmap  20568  rhmsscrnghm  20574  rngcresringcat  20578  srhmsubc  20589  rhmsubclem3  20596  fldhmsubc  20694  mptscmfsupp0  20833  lspss  20890  lspsntrim  21005  aspss  21786  resspsrbas  21883  resspsradd  21884  resspsrmul  21885  clsss  22941  ntrss  22942  sslm  23186  1stcfb  23332  txss12  23492  prdstopn  23515  imasncls  23579  fmss  23833  flfssfcf  23925  cnpfcfi  23927  ressprdsds  24259  metss2lem  24399  metustto  24441  pi1addval  24948  pi1xfrcnv  24957  equivcau  25200  rrxmvallem  25304  uniiccvol  25481  dyaddisjlem  25496  volsup2  25506  itg2monolem1  25651  itg2gt0  25661  plyss  26104  lgamucov  26948  madess  27788  addsbday  27924  ifpsnprss  29551  wlkp1lem7  29607  occon  31216  spanss  31277  shlej1  31289  chscllem1  31566  chscllem2  31567  chscllem3  31568  ofrn2  32564  resf1o  32653  fpwrelmap  32656  ccatdmss  32871  fldgenss  33266  orvclteinc  34467  dstfrvclim1  34469  reprss  34608  reprinfz1  34613  revwlk  35112  ss2mcls  35555  heiborlem6  37810  lpssat  39006  lssat  39009  paddass  39832  pclssN  39888  2polssN  39909  polcon3N  39911  paddunN  39921  dibss  41163  dicssdvh  41180  dih2dimb  41238  dih2dimbALTN  41239  dihord5b  41253  dochss  41359  dochspss  41372  dvh3dim3N  41443  lclkrlem2r  41518  lclkr  41527  lclkrs  41533  hgmaprnlem2N  41891  hbtlem4  43115  hbtlem3  43116  itgoss  43152  omabs2  43321  naddgeoa  43383  naddwordnexlem4  43390  trrelind  43654  trrelsuperreldg  43657  trrelsuperrel2dg  43660  relexpss1d  43694  trclrelexplem  43700  relexpaddss  43707  frege97d  43741  frege109d  43746  frege131d  43753  clsk1indlem3  44032  limclner  45649  fourierdlem49  46153  fourierdlem92  46196  ovolval5lem3  46652  rhmsubcALTVlem4  48272  srhmsubcALTV  48313  fldhmsubcALTV  48321  rmsuppss  48358  scmsuppss  48359  imassc  49142  setrecsss  49690