Theorem 3sstr4d 3968

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

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

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

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

This theorem is used by:  rescnvimafod  7105  suppimacnvss  8228  suppimacnv  8229  ressuppss  8238  suppun  8239  ressuppssdif  8240  suppfnss  8244  suppssov1  8252  suppssov2  8253  suppssfv  8257  omwordri  8618  oewordri  8639  oaabs2  8696  naddssim  8733  fiss  9453  harword  9594  rankval4b  9917  fin1a2lem12  10528  fzoss1  13861  fzoss2  13862  ccatdmss  14768  swrd0  14850  cshimadifsn  15022  trclfvss  15202  trclfvcotrg  15212  relexpnnrn  15241  vdwlem6  17208  vdwlem8  17210  hashbcss  17226  mrcss  17840  chnrev  18851  mndpsuppss  19009  snsymgefmndeq  19660  gsumzf1o  20177  gsumzaddlem  20186  dprdres  20295  dprdz  20297  dprdf1o  20299  rngchomfval  20925  rngccofval  20929  rnghmsscmap2  20932  rnghmsscmap  20933  ringchomfval  20954  ringccofval  20958  rhmsscmap2  20961  rhmsscmap  20962  rhmsscrnghm  20968  rngcresringcat  20972  srhmsubc  20983  rhmsubclem3  20990  fldhmsubc  21093  mptscmfsupp0  21253  lspss  21310  lspsntrim  21424  aspss  22239  resspsrbas  22336  resspsradd  22337  resspsrmul  22338  clsss  23427  ntrss  23428  sslm  23672  1stcfb  23818  txss12  23979  prdstopn  24002  imasncls  24066  fmss  24320  flfssfcf  24412  cnpfcfi  24414  ressprdsds  24745  metss2lem  24885  metustto  24927  pi1addval  25424  pi1xfrcnv  25433  equivcau  25676  rrxmvallem  25780  uniiccvol  25956  dyaddisjlem  25971  volsup2  25981  itg2monolem1  26126  itg2gt0  26136  plyss  26572  lgamucov  27422  madess  28309  oldss  28313  addbday  28461  ifpsnprss  30260  wlkp1lem7  30315  revwlk  30324  occon  31946  spanss  32007  shlej1  32019  chscllem1  32296  chscllem2  32297  chscllem3  32298  ofrn2  33332  resf1o  33418  fpwrelmap  33421  fldgenss  33982  orvclteinc  35219  dstfrvclim1  35221  reprss  35357  reprinfz1  35362  ss2mcls  36541  nmulss1  37178  heiborlem6  39016  lpssat  40336  lssat  40339  paddass  41161  pclssN  41217  2polssN  41238  polcon3N  41240  paddunN  41250  dibss  42492  dicssdvh  42509  dih2dimb  42567  dih2dimbALTN  42568  dihord5b  42582  dochss  42688  dochspss  42701  dvh3dim3N  42772  lclkrlem2r  42847  lclkr  42856  lclkrs  42862  hgmaprnlem2N  43220  hbtlem4  44393  hbtlem3  44394  itgoss  44430  omabs2  44595  naddgeoa  44657  naddwordnexlem4  44664  trrelind  44926  trrelsuperreldg  44929  trrelsuperrel2dg  44932  relexpss1d  44966  trclrelexplem  44972  relexpaddss  44979  frege97d  45013  frege109d  45018  frege131d  45025  clsk1indlem3  45304  limclner  46934  fourierdlem49  47438  fourierdlem92  47481  ovolval5lem3  47937  rhmsubcALTVlem4  49654  srhmsubcALTV  49695  fldhmsubcALTV  49703  rmsuppss  49813  scmsuppss  49814  imassc  50600  setrecsss  51200