Theorem 3sstr4d 4014

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

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

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 2007  ax-9 2118  ax-ext 2707

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

This theorem is referenced by:  rescnvimafod  7063  suppimacnvss  8172  suppimacnv  8173  ressuppss  8182  suppun  8183  ressuppssdif  8184  suppfnss  8188  suppssov1  8196  suppssov2  8197  suppssfv  8201  omwordri  8584  oewordri  8604  oaabs2  8661  naddssim  8697  fiss  9436  harword  9577  fin1a2lem12  10425  fzoss1  13703  fzoss2  13704  swrd0  14676  cshimadifsn  14848  trclfvss  15025  trclfvcotrg  15035  relexpnnrn  15064  vdwlem6  17006  vdwlem8  17008  hashbcss  17024  mrcss  17628  mndpsuppss  18743  snsymgefmndeq  19376  gsumzf1o  19893  gsumzaddlem  19902  dprdres  20011  dprdz  20013  dprdf1o  20015  rngchomfval  20582  rngccofval  20586  rnghmsscmap2  20589  rnghmsscmap  20590  ringchomfval  20611  ringccofval  20615  rhmsscmap2  20618  rhmsscmap  20619  rhmsscrnghm  20625  rngcresringcat  20629  srhmsubc  20640  rhmsubclem3  20647  fldhmsubc  20745  mptscmfsupp0  20884  lspss  20941  lspsntrim  21056  aspss  21837  resspsrbas  21934  resspsradd  21935  resspsrmul  21936  clsss  22992  ntrss  22993  sslm  23237  1stcfb  23383  txss12  23543  prdstopn  23566  imasncls  23630  fmss  23884  flfssfcf  23976  cnpfcfi  23978  ressprdsds  24310  metss2lem  24450  metustto  24492  pi1addval  24999  pi1xfrcnv  25008  equivcau  25252  rrxmvallem  25356  uniiccvol  25533  dyaddisjlem  25548  volsup2  25558  itg2monolem1  25703  itg2gt0  25713  plyss  26156  lgamucov  27000  madess  27840  addsbday  27976  ifpsnprss  29603  wlkp1lem7  29659  occon  31268  spanss  31329  shlej1  31341  chscllem1  31618  chscllem2  31619  chscllem3  31620  ofrn2  32618  resf1o  32707  fpwrelmap  32710  ccatdmss  32925  fldgenss  33310  orvclteinc  34508  dstfrvclim1  34510  reprss  34649  reprinfz1  34654  revwlk  35147  ss2mcls  35590  heiborlem6  37840  lpssat  39031  lssat  39034  paddass  39857  pclssN  39913  2polssN  39934  polcon3N  39936  paddunN  39946  dibss  41188  dicssdvh  41205  dih2dimb  41263  dih2dimbALTN  41264  dihord5b  41278  dochss  41384  dochspss  41397  dvh3dim3N  41468  lclkrlem2r  41543  lclkr  41552  lclkrs  41558  hgmaprnlem2N  41916  hbtlem4  43150  hbtlem3  43151  itgoss  43187  omabs2  43356  naddgeoa  43418  naddwordnexlem4  43425  trrelind  43689  trrelsuperreldg  43692  trrelsuperrel2dg  43695  relexpss1d  43729  trclrelexplem  43735  relexpaddss  43742  frege97d  43776  frege109d  43781  frege131d  43788  clsk1indlem3  44067  limclner  45680  fourierdlem49  46184  fourierdlem92  46227  ovolval5lem3  46683  rhmsubcALTVlem4  48259  srhmsubcALTV  48300  fldhmsubcALTV  48308  rmsuppss  48345  scmsuppss  48346  imassc  49093  setrecsss  49565