Theorem 3sstr4d 3989

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

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

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 2123  ax-ext 2708

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

This theorem is referenced by:  rescnvimafod  7018  suppimacnvss  8115  suppimacnv  8116  ressuppss  8125  suppun  8126  ressuppssdif  8127  suppfnss  8131  suppssov1  8139  suppssov2  8140  suppssfv  8144  omwordri  8499  oewordri  8520  oaabs2  8577  naddssim  8613  fiss  9327  harword  9468  fin1a2lem12  10321  fzoss1  13602  fzoss2  13603  ccatdmss  14505  swrd0  14582  cshimadifsn  14752  trclfvss  14929  trclfvcotrg  14939  relexpnnrn  14968  vdwlem6  16914  vdwlem8  16916  hashbcss  16932  mrcss  17539  chnrev  18550  mndpsuppss  18690  snsymgefmndeq  19324  gsumzf1o  19841  gsumzaddlem  19850  dprdres  19959  dprdz  19961  dprdf1o  19963  rngchomfval  20555  rngccofval  20559  rnghmsscmap2  20562  rnghmsscmap  20563  ringchomfval  20584  ringccofval  20588  rhmsscmap2  20591  rhmsscmap  20592  rhmsscrnghm  20598  rngcresringcat  20602  srhmsubc  20613  rhmsubclem3  20620  fldhmsubc  20718  mptscmfsupp0  20878  lspss  20935  lspsntrim  21050  aspss  21832  resspsrbas  21929  resspsradd  21930  resspsrmul  21931  clsss  22998  ntrss  22999  sslm  23243  1stcfb  23389  txss12  23549  prdstopn  23572  imasncls  23636  fmss  23890  flfssfcf  23982  cnpfcfi  23984  ressprdsds  24315  metss2lem  24455  metustto  24497  pi1addval  25004  pi1xfrcnv  25013  equivcau  25256  rrxmvallem  25360  uniiccvol  25537  dyaddisjlem  25552  volsup2  25562  itg2monolem1  25707  itg2gt0  25717  plyss  26160  lgamucov  27004  madess  27862  oldss  27866  addbday  28014  ifpsnprss  29696  wlkp1lem7  29751  occon  31362  spanss  31423  shlej1  31435  chscllem1  31712  chscllem2  31713  chscllem3  31714  ofrn2  32718  resf1o  32809  fpwrelmap  32812  fldgenss  33398  orvclteinc  34633  dstfrvclim1  34635  reprss  34774  reprinfz1  34779  rankval4b  35256  revwlk  35319  ss2mcls  35762  heiborlem6  38017  lpssat  39273  lssat  39276  paddass  40098  pclssN  40154  2polssN  40175  polcon3N  40177  paddunN  40187  dibss  41429  dicssdvh  41446  dih2dimb  41504  dih2dimbALTN  41505  dihord5b  41519  dochss  41625  dochspss  41638  dvh3dim3N  41709  lclkrlem2r  41784  lclkr  41793  lclkrs  41799  hgmaprnlem2N  42157  hbtlem4  43368  hbtlem3  43369  itgoss  43405  omabs2  43574  naddgeoa  43636  naddwordnexlem4  43643  trrelind  43906  trrelsuperreldg  43909  trrelsuperrel2dg  43912  relexpss1d  43946  trclrelexplem  43952  relexpaddss  43959  frege97d  43993  frege109d  43998  frege131d  44005  clsk1indlem3  44284  limclner  45895  fourierdlem49  46399  fourierdlem92  46442  ovolval5lem3  46898  rhmsubcALTVlem4  48530  srhmsubcALTV  48571  fldhmsubcALTV  48579  rmsuppss  48616  scmsuppss  48617  imassc  49398  setrecsss  49946