Theorem 3sstr4d 3977

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

Syntax hints:   → wi 4   = wceq 1547   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732  df-ss 3907

This theorem is referenced by:  rescnvimafod  7021  suppimacnvss  8120  suppimacnv  8121  ressuppss  8130  suppun  8131  ressuppssdif  8132  suppfnss  8136  suppssov1  8144  suppssov2  8145  suppssfv  8149  omwordri  8504  oewordri  8525  oaabs2  8582  naddssim  8618  fiss  9334  harword  9475  fin1a2lem12  10331  fzoss1  13639  fzoss2  13640  ccatdmss  14542  swrd0  14619  cshimadifsn  14789  trclfvss  14966  trclfvcotrg  14976  relexpnnrn  15005  vdwlem6  16955  vdwlem8  16957  hashbcss  16973  mrcss  17580  chnrev  18591  mndpsuppss  18731  snsymgefmndeq  19368  gsumzf1o  19885  gsumzaddlem  19894  dprdres  20003  dprdz  20005  dprdf1o  20007  rngchomfval  20601  rngccofval  20605  rnghmsscmap2  20608  rnghmsscmap  20609  ringchomfval  20630  ringccofval  20634  rhmsscmap2  20637  rhmsscmap  20638  rhmsscrnghm  20644  rngcresringcat  20648  srhmsubc  20659  rhmsubclem3  20666  fldhmsubc  20764  mptscmfsupp0  20924  lspss  20981  lspsntrim  21095  aspss  21858  resspsrbas  21955  resspsradd  21956  resspsrmul  21957  clsss  23044  ntrss  23045  sslm  23289  1stcfb  23435  txss12  23595  prdstopn  23618  imasncls  23682  fmss  23936  flfssfcf  24028  cnpfcfi  24030  ressprdsds  24361  metss2lem  24501  metustto  24543  pi1addval  25040  pi1xfrcnv  25049  equivcau  25292  rrxmvallem  25396  uniiccvol  25572  dyaddisjlem  25587  volsup2  25597  itg2monolem1  25742  itg2gt0  25752  plyss  26189  lgamucov  27026  madess  27883  oldss  27887  addbday  28035  ifpsnprss  29716  wlkp1lem7  29771  occon  31383  spanss  31444  shlej1  31456  chscllem1  31733  chscllem2  31734  chscllem3  31735  ofrn2  32739  resf1o  32829  fpwrelmap  32832  fldgenss  33407  orvclteinc  34667  dstfrvclim1  34669  reprss  34808  reprinfz1  34813  rankval4b  35288  revwlk  35360  ss2mcls  35803  heiborlem6  38190  lpssat  39512  lssat  39515  paddass  40337  pclssN  40393  2polssN  40414  polcon3N  40416  paddunN  40426  dibss  41668  dicssdvh  41685  dih2dimb  41743  dih2dimbALTN  41744  dihord5b  41758  dochss  41864  dochspss  41877  dvh3dim3N  41948  lclkrlem2r  42023  lclkr  42032  lclkrs  42038  hgmaprnlem2N  42396  hbtlem4  43578  hbtlem3  43579  itgoss  43615  omabs2  43784  naddgeoa  43846  naddwordnexlem4  43853  trrelind  44116  trrelsuperreldg  44119  trrelsuperrel2dg  44122  relexpss1d  44156  trclrelexplem  44162  relexpaddss  44169  frege97d  44203  frege109d  44208  frege131d  44215  clsk1indlem3  44494  limclner  46101  fourierdlem49  46605  fourierdlem92  46648  ovolval5lem3  47104  rhmsubcALTVlem4  48782  srhmsubcALTV  48823  fldhmsubcALTV  48831  rmsuppss  48868  scmsuppss  48869  imassc  49650  setrecsss  50198