Theorem 3sstr4d 3986

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

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

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 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

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

This theorem is used by:  rescnvimafod  7071  suppimacnvss  8183  suppimacnv  8184  ressuppss  8193  suppun  8194  ressuppssdif  8195  suppfnss  8199  suppssov1  8207  suppssov2  8208  suppssfv  8212  omwordri  8573  oewordri  8594  oaabs2  8651  naddssim  8688  fiss  9409  harword  9550  rankval4b  9873  fin1a2lem12  10482  fzoss1  13814  fzoss2  13815  ccatdmss  14720  swrd0  14801  cshimadifsn  14973  trclfvss  15152  trclfvcotrg  15162  relexpnnrn  15191  vdwlem6  17157  vdwlem8  17159  hashbcss  17175  mrcss  17783  chnrev  18794  mndpsuppss  18952  snsymgefmndeq  19602  gsumzf1o  20119  gsumzaddlem  20128  dprdres  20237  dprdz  20239  dprdf1o  20241  rngchomfval  20867  rngccofval  20871  rnghmsscmap2  20874  rnghmsscmap  20875  ringchomfval  20896  ringccofval  20900  rhmsscmap2  20903  rhmsscmap  20904  rhmsscrnghm  20910  rngcresringcat  20914  srhmsubc  20925  rhmsubclem3  20932  fldhmsubc  21035  mptscmfsupp0  21195  lspss  21252  lspsntrim  21366  aspss  22177  resspsrbas  22274  resspsradd  22275  resspsrmul  22276  clsss  23365  ntrss  23366  sslm  23610  1stcfb  23756  txss12  23917  prdstopn  23940  imasncls  24004  fmss  24258  flfssfcf  24350  cnpfcfi  24352  ressprdsds  24683  metss2lem  24823  metustto  24865  pi1addval  25362  pi1xfrcnv  25371  equivcau  25614  rrxmvallem  25718  uniiccvol  25894  dyaddisjlem  25909  volsup2  25919  itg2monolem1  26064  itg2gt0  26074  plyss  26510  lgamucov  27358  madess  28245  oldss  28249  addbday  28397  ifpsnprss  30196  wlkp1lem7  30251  revwlk  30260  occon  31882  spanss  31943  shlej1  31955  chscllem1  32232  chscllem2  32233  chscllem3  32234  ofrn2  33227  resf1o  33315  fpwrelmap  33318  fldgenss  33871  orvclteinc  35101  dstfrvclim1  35103  reprss  35239  reprinfz1  35244  ss2mcls  36312  nmulss1  36943  heiborlem6  38730  lpssat  40050  lssat  40053  paddass  40875  pclssN  40931  2polssN  40952  polcon3N  40954  paddunN  40964  dibss  42206  dicssdvh  42223  dih2dimb  42281  dih2dimbALTN  42282  dihord5b  42296  dochss  42402  dochspss  42415  dvh3dim3N  42486  lclkrlem2r  42561  lclkr  42570  lclkrs  42576  hgmaprnlem2N  42934  hbtlem4  44112  hbtlem3  44113  itgoss  44149  omabs2  44318  naddgeoa  44380  naddwordnexlem4  44387  trrelind  44650  trrelsuperreldg  44653  trrelsuperrel2dg  44656  relexpss1d  44690  trclrelexplem  44696  relexpaddss  44703  frege97d  44737  frege109d  44742  frege131d  44749  clsk1indlem3  45028  limclner  46630  fourierdlem49  47134  fourierdlem92  47177  ovolval5lem3  47633  rhmsubcALTVlem4  49350  srhmsubcALTV  49391  fldhmsubcALTV  49399  rmsuppss  49451  scmsuppss  49452  imassc  50230  setrecsss  50763