Theorem 3sstr4d 3990

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-ss 3919

This theorem is referenced by:  rescnvimafod  7006  suppimacnvss  8103  suppimacnv  8104  ressuppss  8113  suppun  8114  ressuppssdif  8115  suppfnss  8119  suppssov1  8127  suppssov2  8128  suppssfv  8132  omwordri  8487  oewordri  8507  oaabs2  8564  naddssim  8600  fiss  9308  harword  9449  fin1a2lem12  10302  fzoss1  13586  fzoss2  13587  ccatdmss  14489  swrd0  14566  cshimadifsn  14736  trclfvss  14913  trclfvcotrg  14923  relexpnnrn  14952  vdwlem6  16898  vdwlem8  16900  hashbcss  16916  mrcss  17522  chnrev  18533  mndpsuppss  18673  snsymgefmndeq  19308  gsumzf1o  19825  gsumzaddlem  19834  dprdres  19943  dprdz  19945  dprdf1o  19947  rngchomfval  20538  rngccofval  20542  rnghmsscmap2  20545  rnghmsscmap  20546  ringchomfval  20567  ringccofval  20571  rhmsscmap2  20574  rhmsscmap  20575  rhmsscrnghm  20581  rngcresringcat  20585  srhmsubc  20596  rhmsubclem3  20603  fldhmsubc  20701  mptscmfsupp0  20861  lspss  20918  lspsntrim  21033  aspss  21815  resspsrbas  21912  resspsradd  21913  resspsrmul  21914  clsss  22970  ntrss  22971  sslm  23215  1stcfb  23361  txss12  23521  prdstopn  23544  imasncls  23608  fmss  23862  flfssfcf  23954  cnpfcfi  23956  ressprdsds  24287  metss2lem  24427  metustto  24469  pi1addval  24976  pi1xfrcnv  24985  equivcau  25228  rrxmvallem  25332  uniiccvol  25509  dyaddisjlem  25524  volsup2  25534  itg2monolem1  25679  itg2gt0  25689  plyss  26132  lgamucov  26976  madess  27822  oldss  27824  addsbday  27961  ifpsnprss  29602  wlkp1lem7  29657  occon  31265  spanss  31326  shlej1  31338  chscllem1  31615  chscllem2  31616  chscllem3  31617  ofrn2  32620  resf1o  32711  fpwrelmap  32714  fldgenss  33280  orvclteinc  34487  dstfrvclim1  34489  reprss  34628  reprinfz1  34633  rankval4b  35109  revwlk  35167  ss2mcls  35610  heiborlem6  37862  lpssat  39058  lssat  39061  paddass  39883  pclssN  39939  2polssN  39960  polcon3N  39962  paddunN  39972  dibss  41214  dicssdvh  41231  dih2dimb  41289  dih2dimbALTN  41290  dihord5b  41304  dochss  41410  dochspss  41423  dvh3dim3N  41494  lclkrlem2r  41569  lclkr  41578  lclkrs  41584  hgmaprnlem2N  41942  hbtlem4  43165  hbtlem3  43166  itgoss  43202  omabs2  43371  naddgeoa  43433  naddwordnexlem4  43440  trrelind  43704  trrelsuperreldg  43707  trrelsuperrel2dg  43710  relexpss1d  43744  trclrelexplem  43750  relexpaddss  43757  frege97d  43791  frege109d  43796  frege131d  43803  clsk1indlem3  44082  limclner  45695  fourierdlem49  46199  fourierdlem92  46242  ovolval5lem3  46698  rhmsubcALTVlem4  48321  srhmsubcALTV  48362  fldhmsubcALTV  48370  rmsuppss  48407  scmsuppss  48408  imassc  49191  setrecsss  49739