Theorem 3sstr4d 4039

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

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

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 2708

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

This theorem is referenced by:  rescnvimafod  7093  suppimacnvss  8198  suppimacnv  8199  ressuppss  8208  suppun  8209  ressuppssdif  8210  suppfnss  8214  suppssov1  8222  suppssov2  8223  suppssfv  8227  omwordri  8610  oewordri  8630  oaabs2  8687  naddssim  8723  fiss  9464  harword  9603  fin1a2lem12  10451  fzoss1  13726  fzoss2  13727  swrd0  14696  cshimadifsn  14868  trclfvss  15045  trclfvcotrg  15055  relexpnnrn  15084  vdwlem6  17024  vdwlem8  17026  hashbcss  17042  mrcss  17659  mndpsuppss  18778  snsymgefmndeq  19412  gsumzf1o  19930  gsumzaddlem  19939  dprdres  20048  dprdz  20050  dprdf1o  20052  rngchomfval  20622  rngccofval  20626  rnghmsscmap2  20629  rnghmsscmap  20630  ringchomfval  20651  ringccofval  20655  rhmsscmap2  20658  rhmsscmap  20659  rhmsscrnghm  20665  rngcresringcat  20669  srhmsubc  20680  rhmsubclem3  20687  fldhmsubc  20786  mptscmfsupp0  20925  lspss  20982  lspsntrim  21097  aspss  21897  resspsrbas  21994  resspsradd  21995  resspsrmul  21996  clsss  23062  ntrss  23063  sslm  23307  1stcfb  23453  txss12  23613  prdstopn  23636  imasncls  23700  fmss  23954  flfssfcf  24046  cnpfcfi  24048  ressprdsds  24381  metss2lem  24524  metustto  24566  pi1addval  25081  pi1xfrcnv  25090  equivcau  25334  rrxmvallem  25438  uniiccvol  25615  dyaddisjlem  25630  volsup2  25640  itg2monolem1  25785  itg2gt0  25795  plyss  26238  lgamucov  27081  madess  27915  addsbday  28050  ifpsnprss  29641  wlkp1lem7  29697  occon  31306  spanss  31367  shlej1  31379  chscllem1  31656  chscllem2  31657  chscllem3  31658  ofrn2  32650  resf1o  32741  fpwrelmap  32744  ccatdmss  32934  fldgenss  33318  orvclteinc  34478  dstfrvclim1  34480  reprss  34632  reprinfz1  34637  revwlk  35130  ss2mcls  35573  heiborlem6  37823  lpssat  39014  lssat  39017  paddass  39840  pclssN  39896  2polssN  39917  polcon3N  39919  paddunN  39929  dibss  41171  dicssdvh  41188  dih2dimb  41246  dih2dimbALTN  41247  dihord5b  41261  dochss  41367  dochspss  41380  dvh3dim3N  41451  lclkrlem2r  41526  lclkr  41535  lclkrs  41541  hgmaprnlem2N  41899  hbtlem4  43138  hbtlem3  43139  itgoss  43175  omabs2  43345  naddgeoa  43407  naddwordnexlem4  43414  trrelind  43678  trrelsuperreldg  43681  trrelsuperrel2dg  43684  relexpss1d  43718  trclrelexplem  43724  relexpaddss  43731  frege97d  43765  frege109d  43770  frege131d  43777  clsk1indlem3  44056  limclner  45666  fourierdlem49  46170  fourierdlem92  46213  ovolval5lem3  46669  rhmsubcALTVlem4  48200  srhmsubcALTV  48241  fldhmsubcALTV  48249  rmsuppss  48286  scmsuppss  48287  setrecsss  49220