Theorem 3sstr4d 3989

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

Syntax hints:   → wi 4   = wceq 1559   ⊆ wss 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-ss 3919

This theorem is referenced by:  rescnvimafod  7048  suppimacnvss  8146  suppimacnv  8147  ressuppss  8156  suppun  8157  ressuppssdif  8158  suppfnss  8162  suppssov1  8170  suppssov2  8171  suppssfv  8175  omwordri  8534  oewordri  8555  oaabs2  8612  naddssim  8649  fiss  9363  harword  9504  fin1a2lem12  10361  fzoss1  13685  fzoss2  13686  ccatdmss  14588  swrd0  14665  cshimadifsn  14835  trclfvss  15012  trclfvcotrg  15022  relexpnnrn  15051  vdwlem6  17012  vdwlem8  17014  hashbcss  17030  mrcss  17638  chnrev  18649  mndpsuppss  18789  snsymgefmndeq  19425  gsumzf1o  19942  gsumzaddlem  19951  dprdres  20060  dprdz  20062  dprdf1o  20064  rngchomfval  20658  rngccofval  20662  rnghmsscmap2  20665  rnghmsscmap  20666  ringchomfval  20687  ringccofval  20691  rhmsscmap2  20694  rhmsscmap  20695  rhmsscrnghm  20701  rngcresringcat  20705  srhmsubc  20716  rhmsubclem3  20723  fldhmsubc  20821  mptscmfsupp0  20981  lspss  21038  lspsntrim  21152  aspss  21915  resspsrbas  22012  resspsradd  22013  resspsrmul  22014  clsss  23101  ntrss  23102  sslm  23346  1stcfb  23492  txss12  23652  prdstopn  23675  imasncls  23739  fmss  23993  flfssfcf  24085  cnpfcfi  24087  ressprdsds  24418  metss2lem  24558  metustto  24600  pi1addval  25097  pi1xfrcnv  25106  equivcau  25349  rrxmvallem  25453  uniiccvol  25629  dyaddisjlem  25644  volsup2  25654  itg2monolem1  25799  itg2gt0  25809  plyss  26246  lgamucov  27089  madess  27946  oldss  27950  addbday  28098  ifpsnprss  29779  wlkp1lem7  29834  occon  31446  spanss  31507  shlej1  31519  chscllem1  31796  chscllem2  31797  chscllem3  31798  ofrn2  32802  resf1o  32892  fpwrelmap  32895  fldgenss  33463  orvclteinc  34733  dstfrvclim1  34735  reprss  34871  reprinfz1  34876  rankval4b  35356  revwlk  35435  ss2mcls  35878  heiborlem6  38275  lpssat  39597  lssat  39600  paddass  40422  pclssN  40478  2polssN  40499  polcon3N  40501  paddunN  40511  dibss  41753  dicssdvh  41770  dih2dimb  41828  dih2dimbALTN  41829  dihord5b  41843  dochss  41949  dochspss  41962  dvh3dim3N  42033  lclkrlem2r  42108  lclkr  42117  lclkrs  42123  hgmaprnlem2N  42481  hbtlem4  43663  hbtlem3  43664  itgoss  43700  omabs2  43869  naddgeoa  43931  naddwordnexlem4  43938  trrelind  44201  trrelsuperreldg  44204  trrelsuperrel2dg  44207  relexpss1d  44241  trclrelexplem  44247  relexpaddss  44254  frege97d  44288  frege109d  44293  frege131d  44300  clsk1indlem3  44579  limclner  46185  fourierdlem49  46689  fourierdlem92  46732  ovolval5lem3  47188  rhmsubcALTVlem4  48866  srhmsubcALTV  48907  fldhmsubcALTV  48915  rmsuppss  48952  scmsuppss  48953  imassc  49734  setrecsss  50282