Theorem 3sstr4d 3986

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-ss 3916

This theorem is used by:  rescnvimafod  7066  suppimacnvss  8171  suppimacnv  8172  ressuppss  8181  suppun  8182  ressuppssdif  8183  suppfnss  8187  suppssov1  8195  suppssov2  8196  suppssfv  8200  omwordri  8559  oewordri  8580  oaabs2  8637  naddssim  8674  fiss  9394  harword  9535  fin1a2lem12  10413  fzoss1  13742  fzoss2  13743  ccatdmss  14647  swrd0  14728  cshimadifsn  14900  trclfvss  15079  trclfvcotrg  15089  relexpnnrn  15118  vdwlem6  17078  vdwlem8  17080  hashbcss  17096  mrcss  17704  chnrev  18715  mndpsuppss  18872  snsymgefmndeq  19522  gsumzf1o  20039  gsumzaddlem  20048  dprdres  20157  dprdz  20159  dprdf1o  20161  rngchomfval  20784  rngccofval  20788  rnghmsscmap2  20791  rnghmsscmap  20792  ringchomfval  20813  ringccofval  20817  rhmsscmap2  20820  rhmsscmap  20821  rhmsscrnghm  20827  rngcresringcat  20831  srhmsubc  20842  rhmsubclem3  20849  fldhmsubc  20951  mptscmfsupp0  21111  lspss  21168  lspsntrim  21282  aspss  22091  resspsrbas  22188  resspsradd  22189  resspsrmul  22190  clsss  23279  ntrss  23280  sslm  23524  1stcfb  23670  txss12  23831  prdstopn  23854  imasncls  23918  fmss  24172  flfssfcf  24264  cnpfcfi  24266  ressprdsds  24597  metss2lem  24737  metustto  24779  pi1addval  25276  pi1xfrcnv  25285  equivcau  25528  rrxmvallem  25632  uniiccvol  25808  dyaddisjlem  25823  volsup2  25833  itg2monolem1  25978  itg2gt0  25988  plyss  26424  lgamucov  27274  madess  28131  oldss  28135  addbday  28283  ifpsnprss  30082  wlkp1lem7  30137  revwlk  30146  occon  31768  spanss  31829  shlej1  31841  chscllem1  32118  chscllem2  32119  chscllem3  32120  ofrn2  33113  resf1o  33201  fpwrelmap  33204  fldgenss  33757  orvclteinc  34987  dstfrvclim1  34989  reprss  35125  reprinfz1  35130  rankval4b  35607  ss2mcls  36147  nmulss1  36794  heiborlem6  38566  lpssat  39886  lssat  39889  paddass  40711  pclssN  40767  2polssN  40788  polcon3N  40790  paddunN  40800  dibss  42042  dicssdvh  42059  dih2dimb  42117  dih2dimbALTN  42118  dihord5b  42132  dochss  42238  dochspss  42251  dvh3dim3N  42322  lclkrlem2r  42397  lclkr  42406  lclkrs  42412  hgmaprnlem2N  42770  hbtlem4  43967  hbtlem3  43968  itgoss  44004  omabs2  44173  naddgeoa  44235  naddwordnexlem4  44242  trrelind  44505  trrelsuperreldg  44508  trrelsuperrel2dg  44511  relexpss1d  44545  trclrelexplem  44551  relexpaddss  44558  frege97d  44592  frege109d  44597  frege131d  44604  clsk1indlem3  44883  limclner  46479  fourierdlem49  46983  fourierdlem92  47026  ovolval5lem3  47482  rhmsubcALTVlem4  49199  srhmsubcALTV  49240  fldhmsubcALTV  49248  rmsuppss  49300  scmsuppss  49301  imassc  50079  setrecsss  50627