Theorem 3sstr4d 3993

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

Syntax hints:   → wi 4   = wceq 1570   ⊆ wss 3906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ss 3923

This theorem is referenced by:  rescnvimafod  7070  suppimacnvss  8170  suppimacnv  8171  ressuppss  8180  suppun  8181  ressuppssdif  8182  suppfnss  8186  suppssov1  8194  suppssov2  8195  suppssfv  8199  omwordri  8558  oewordri  8579  oaabs2  8636  naddssim  8673  fiss  9385  harword  9526  fin1a2lem12  10396  fzoss1  13717  fzoss2  13718  ccatdmss  14621  swrd0  14698  cshimadifsn  14868  trclfvss  15045  trclfvcotrg  15055  relexpnnrn  15084  vdwlem6  17047  vdwlem8  17049  hashbcss  17065  mrcss  17673  chnrev  18684  mndpsuppss  18824  snsymgefmndeq  19466  gsumzf1o  19983  gsumzaddlem  19992  dprdres  20101  dprdz  20103  dprdf1o  20105  rngchomfval  20708  rngccofval  20712  rnghmsscmap2  20715  rnghmsscmap  20716  ringchomfval  20737  ringccofval  20741  rhmsscmap2  20744  rhmsscmap  20745  rhmsscrnghm  20751  rngcresringcat  20755  srhmsubc  20766  rhmsubclem3  20773  fldhmsubc  20869  mptscmfsupp0  21029  lspss  21086  lspsntrim  21200  aspss  22007  resspsrbas  22104  resspsradd  22105  resspsrmul  22106  clsss  23192  ntrss  23193  sslm  23437  1stcfb  23583  txss12  23743  prdstopn  23766  imasncls  23830  fmss  24084  flfssfcf  24176  cnpfcfi  24178  ressprdsds  24509  metss2lem  24649  metustto  24691  pi1addval  25188  pi1xfrcnv  25197  equivcau  25440  rrxmvallem  25544  uniiccvol  25720  dyaddisjlem  25735  volsup2  25745  itg2monolem1  25890  itg2gt0  25900  plyss  26337  lgamucov  27183  madess  28040  oldss  28044  addbday  28192  ifpsnprss  29953  wlkp1lem7  30008  occon  31620  spanss  31681  shlej1  31693  chscllem1  31970  chscllem2  31971  chscllem3  31972  ofrn2  32966  resf1o  33056  fpwrelmap  33059  fldgenss  33618  orvclteinc  34847  dstfrvclim1  34849  reprss  34985  reprinfz1  34990  rankval4b  35474  revwlk  35598  ss2mcls  36041  nmulss1  36672  heiborlem6  38448  lpssat  39768  lssat  39771  paddass  40593  pclssN  40649  2polssN  40670  polcon3N  40672  paddunN  40682  dibss  41924  dicssdvh  41941  dih2dimb  41999  dih2dimbALTN  42000  dihord5b  42014  dochss  42120  dochspss  42133  dvh3dim3N  42204  lclkrlem2r  42279  lclkr  42288  lclkrs  42294  hgmaprnlem2N  42652  hbtlem4  43836  hbtlem3  43837  itgoss  43873  omabs2  44042  naddgeoa  44104  naddwordnexlem4  44111  trrelind  44374  trrelsuperreldg  44377  trrelsuperrel2dg  44380  relexpss1d  44414  trclrelexplem  44420  relexpaddss  44427  frege97d  44461  frege109d  44466  frege131d  44473  clsk1indlem3  44752  limclner  46348  fourierdlem49  46852  fourierdlem92  46895  ovolval5lem3  47351  rhmsubcALTVlem4  49032  srhmsubcALTV  49073  fldhmsubcALTV  49081  rmsuppss  49133  scmsuppss  49134  imassc  49914  setrecsss  50462