Theorem 3sstr4d 3978

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

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3907

This theorem is referenced by:  rescnvimafod  7019  suppimacnvss  8116  suppimacnv  8117  ressuppss  8126  suppun  8127  ressuppssdif  8128  suppfnss  8132  suppssov1  8140  suppssov2  8141  suppssfv  8145  omwordri  8500  oewordri  8521  oaabs2  8578  naddssim  8614  fiss  9330  harword  9471  fin1a2lem12  10324  fzoss1  13632  fzoss2  13633  ccatdmss  14535  swrd0  14612  cshimadifsn  14782  trclfvss  14959  trclfvcotrg  14969  relexpnnrn  14998  vdwlem6  16948  vdwlem8  16950  hashbcss  16966  mrcss  17573  chnrev  18584  mndpsuppss  18724  snsymgefmndeq  19361  gsumzf1o  19878  gsumzaddlem  19887  dprdres  19996  dprdz  19998  dprdf1o  20000  rngchomfval  20590  rngccofval  20594  rnghmsscmap2  20597  rnghmsscmap  20598  ringchomfval  20619  ringccofval  20623  rhmsscmap2  20626  rhmsscmap  20627  rhmsscrnghm  20633  rngcresringcat  20637  srhmsubc  20648  rhmsubclem3  20655  fldhmsubc  20753  mptscmfsupp0  20913  lspss  20970  lspsntrim  21085  aspss  21866  resspsrbas  21962  resspsradd  21963  resspsrmul  21964  clsss  23029  ntrss  23030  sslm  23274  1stcfb  23420  txss12  23580  prdstopn  23603  imasncls  23667  fmss  23921  flfssfcf  24013  cnpfcfi  24015  ressprdsds  24346  metss2lem  24486  metustto  24528  pi1addval  25025  pi1xfrcnv  25034  equivcau  25277  rrxmvallem  25381  uniiccvol  25557  dyaddisjlem  25572  volsup2  25582  itg2monolem1  25727  itg2gt0  25737  plyss  26174  lgamucov  27015  madess  27872  oldss  27876  addbday  28024  ifpsnprss  29706  wlkp1lem7  29761  occon  31373  spanss  31434  shlej1  31446  chscllem1  31723  chscllem2  31724  chscllem3  31725  ofrn2  32728  resf1o  32818  fpwrelmap  32821  fldgenss  33392  orvclteinc  34636  dstfrvclim1  34638  reprss  34777  reprinfz1  34782  rankval4b  35259  revwlk  35323  ss2mcls  35766  heiborlem6  38151  lpssat  39473  lssat  39476  paddass  40298  pclssN  40354  2polssN  40375  polcon3N  40377  paddunN  40387  dibss  41629  dicssdvh  41646  dih2dimb  41704  dih2dimbALTN  41705  dihord5b  41719  dochss  41825  dochspss  41838  dvh3dim3N  41909  lclkrlem2r  41984  lclkr  41993  lclkrs  41999  hgmaprnlem2N  42357  hbtlem4  43572  hbtlem3  43573  itgoss  43609  omabs2  43778  naddgeoa  43840  naddwordnexlem4  43847  trrelind  44110  trrelsuperreldg  44113  trrelsuperrel2dg  44116  relexpss1d  44150  trclrelexplem  44156  relexpaddss  44163  frege97d  44197  frege109d  44202  frege131d  44209  clsk1indlem3  44488  limclner  46097  fourierdlem49  46601  fourierdlem92  46644  ovolval5lem3  47100  rhmsubcALTVlem4  48772  srhmsubcALTV  48813  fldhmsubcALTV  48821  rmsuppss  48858  scmsuppss  48859  imassc  49640  setrecsss  50188