Theorem 3sstr4d 4005

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

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

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 2702

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

This theorem is referenced by:  rescnvimafod  7048  suppimacnvss  8155  suppimacnv  8156  ressuppss  8165  suppun  8166  ressuppssdif  8167  suppfnss  8171  suppssov1  8179  suppssov2  8180  suppssfv  8184  omwordri  8539  oewordri  8559  oaabs2  8616  naddssim  8652  fiss  9382  harword  9523  fin1a2lem12  10371  fzoss1  13654  fzoss2  13655  swrd0  14630  cshimadifsn  14802  trclfvss  14979  trclfvcotrg  14989  relexpnnrn  15018  vdwlem6  16964  vdwlem8  16966  hashbcss  16982  mrcss  17584  mndpsuppss  18699  snsymgefmndeq  19332  gsumzf1o  19849  gsumzaddlem  19858  dprdres  19967  dprdz  19969  dprdf1o  19971  rngchomfval  20538  rngccofval  20542  rnghmsscmap2  20545  rnghmsscmap  20546  ringchomfval  20567  ringccofval  20571  rhmsscmap2  20574  rhmsscmap  20575  rhmsscrnghm  20581  rngcresringcat  20585  srhmsubc  20596  rhmsubclem3  20603  fldhmsubc  20701  mptscmfsupp0  20840  lspss  20897  lspsntrim  21012  aspss  21793  resspsrbas  21890  resspsradd  21891  resspsrmul  21892  clsss  22948  ntrss  22949  sslm  23193  1stcfb  23339  txss12  23499  prdstopn  23522  imasncls  23586  fmss  23840  flfssfcf  23932  cnpfcfi  23934  ressprdsds  24266  metss2lem  24406  metustto  24448  pi1addval  24955  pi1xfrcnv  24964  equivcau  25207  rrxmvallem  25311  uniiccvol  25488  dyaddisjlem  25503  volsup2  25513  itg2monolem1  25658  itg2gt0  25668  plyss  26111  lgamucov  26955  madess  27795  addsbday  27931  ifpsnprss  29558  wlkp1lem7  29614  occon  31223  spanss  31284  shlej1  31296  chscllem1  31573  chscllem2  31574  chscllem3  31575  ofrn2  32571  resf1o  32660  fpwrelmap  32663  ccatdmss  32878  fldgenss  33273  orvclteinc  34474  dstfrvclim1  34476  reprss  34615  reprinfz1  34620  revwlk  35119  ss2mcls  35562  heiborlem6  37817  lpssat  39013  lssat  39016  paddass  39839  pclssN  39895  2polssN  39916  polcon3N  39918  paddunN  39928  dibss  41170  dicssdvh  41187  dih2dimb  41245  dih2dimbALTN  41246  dihord5b  41260  dochss  41366  dochspss  41379  dvh3dim3N  41450  lclkrlem2r  41525  lclkr  41534  lclkrs  41540  hgmaprnlem2N  41898  hbtlem4  43122  hbtlem3  43123  itgoss  43159  omabs2  43328  naddgeoa  43390  naddwordnexlem4  43397  trrelind  43661  trrelsuperreldg  43664  trrelsuperrel2dg  43667  relexpss1d  43701  trclrelexplem  43707  relexpaddss  43714  frege97d  43748  frege109d  43753  frege131d  43760  clsk1indlem3  44039  limclner  45656  fourierdlem49  46160  fourierdlem92  46203  ovolval5lem3  46659  rhmsubcALTVlem4  48276  srhmsubcALTV  48317  fldhmsubcALTV  48325  rmsuppss  48362  scmsuppss  48363  imassc  49146  setrecsss  49694