Theorem 3sstr4d 3991

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

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

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

This theorem is referenced by:  rescnvimafod  7029  suppimacnvss  8127  suppimacnv  8128  ressuppss  8137  suppun  8138  ressuppssdif  8139  suppfnss  8143  suppssov1  8151  suppssov2  8152  suppssfv  8156  omwordri  8511  oewordri  8532  oaabs2  8589  naddssim  8625  fiss  9341  harword  9482  fin1a2lem12  10335  fzoss1  13616  fzoss2  13617  ccatdmss  14519  swrd0  14596  cshimadifsn  14766  trclfvss  14943  trclfvcotrg  14953  relexpnnrn  14982  vdwlem6  16928  vdwlem8  16930  hashbcss  16946  mrcss  17553  chnrev  18564  mndpsuppss  18704  snsymgefmndeq  19341  gsumzf1o  19858  gsumzaddlem  19867  dprdres  19976  dprdz  19978  dprdf1o  19980  rngchomfval  20572  rngccofval  20576  rnghmsscmap2  20579  rnghmsscmap  20580  ringchomfval  20601  ringccofval  20605  rhmsscmap2  20608  rhmsscmap  20609  rhmsscrnghm  20615  rngcresringcat  20619  srhmsubc  20630  rhmsubclem3  20637  fldhmsubc  20735  mptscmfsupp0  20895  lspss  20952  lspsntrim  21067  aspss  21849  resspsrbas  21946  resspsradd  21947  resspsrmul  21948  clsss  23015  ntrss  23016  sslm  23260  1stcfb  23406  txss12  23566  prdstopn  23589  imasncls  23653  fmss  23907  flfssfcf  23999  cnpfcfi  24001  ressprdsds  24332  metss2lem  24472  metustto  24514  pi1addval  25021  pi1xfrcnv  25030  equivcau  25273  rrxmvallem  25377  uniiccvol  25554  dyaddisjlem  25569  volsup2  25579  itg2monolem1  25724  itg2gt0  25734  plyss  26177  lgamucov  27021  madess  27879  oldss  27883  addbday  28031  ifpsnprss  29714  wlkp1lem7  29769  occon  31381  spanss  31442  shlej1  31454  chscllem1  31731  chscllem2  31732  chscllem3  31733  ofrn2  32736  resf1o  32826  fpwrelmap  32829  fldgenss  33416  orvclteinc  34660  dstfrvclim1  34662  reprss  34801  reprinfz1  34806  rankval4b  35283  revwlk  35347  ss2mcls  35790  heiborlem6  38096  lpssat  39418  lssat  39421  paddass  40243  pclssN  40299  2polssN  40320  polcon3N  40322  paddunN  40332  dibss  41574  dicssdvh  41591  dih2dimb  41649  dih2dimbALTN  41650  dihord5b  41664  dochss  41770  dochspss  41783  dvh3dim3N  41854  lclkrlem2r  41929  lclkr  41938  lclkrs  41944  hgmaprnlem2N  42302  hbtlem4  43512  hbtlem3  43513  itgoss  43549  omabs2  43718  naddgeoa  43780  naddwordnexlem4  43787  trrelind  44050  trrelsuperreldg  44053  trrelsuperrel2dg  44056  relexpss1d  44090  trclrelexplem  44096  relexpaddss  44103  frege97d  44137  frege109d  44142  frege131d  44149  clsk1indlem3  44428  limclner  46038  fourierdlem49  46542  fourierdlem92  46585  ovolval5lem3  47041  rhmsubcALTVlem4  48673  srhmsubcALTV  48714  fldhmsubcALTV  48722  rmsuppss  48759  scmsuppss  48760  imassc  49541  setrecsss  50089