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 ⊢ (𝜑 → 𝐶 ⊆ 𝐷)

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

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 2156  ax-ext 2737

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

This theorem is used by:  rescnvimafod  7072  suppimacnvss  8171  suppimacnv  8172  ressuppss  8181  suppun  8182  ressuppssdif  8183  suppfnss  8187  suppssov1  8195  suppssov2  8196  suppssfv  8200  omwordri  8559  oewordri  8580  oaabs2  8637  naddssim  8674  fiss  9387  harword  9528  fin1a2lem12  10406  fzoss1  13727  fzoss2  13728  ccatdmss  14632  swrd0  14713  cshimadifsn  14885  trclfvss  15062  trclfvcotrg  15072  relexpnnrn  15101  vdwlem6  17063  vdwlem8  17065  hashbcss  17081  mrcss  17689  chnrev  18700  mndpsuppss  18846  snsymgefmndeq  19488  gsumzf1o  20005  gsumzaddlem  20014  dprdres  20123  dprdz  20125  dprdf1o  20127  rngchomfval  20750  rngccofval  20754  rnghmsscmap2  20757  rnghmsscmap  20758  ringchomfval  20779  ringccofval  20783  rhmsscmap2  20786  rhmsscmap  20787  rhmsscrnghm  20793  rngcresringcat  20797  srhmsubc  20808  rhmsubclem3  20815  fldhmsubc  20917  mptscmfsupp0  21077  lspss  21134  lspsntrim  21248  aspss  22055  resspsrbas  22152  resspsradd  22153  resspsrmul  22154  clsss  23240  ntrss  23241  sslm  23485  1stcfb  23631  txss12  23791  prdstopn  23814  imasncls  23878  fmss  24132  flfssfcf  24224  cnpfcfi  24226  ressprdsds  24557  metss2lem  24697  metustto  24739  pi1addval  25236  pi1xfrcnv  25245  equivcau  25488  rrxmvallem  25592  uniiccvol  25768  dyaddisjlem  25783  volsup2  25793  itg2monolem1  25938  itg2gt0  25948  plyss  26385  lgamucov  27231  madess  28088  oldss  28092  addbday  28240  ifpsnprss  30001  wlkp1lem7  30056  occon  31668  spanss  31729  shlej1  31741  chscllem1  32018  chscllem2  32019  chscllem3  32020  ofrn2  33014  resf1o  33104  fpwrelmap  33107  fldgenss  33660  orvclteinc  34890  dstfrvclim1  34892  reprss  35028  reprinfz1  35033  rankval4b  35510  revwlk  35630  ss2mcls  36073  nmulss1  36719  heiborlem6  38500  lpssat  39820  lssat  39823  paddass  40645  pclssN  40701  2polssN  40722  polcon3N  40724  paddunN  40734  dibss  41976  dicssdvh  41993  dih2dimb  42051  dih2dimbALTN  42052  dihord5b  42066  dochss  42172  dochspss  42185  dvh3dim3N  42256  lclkrlem2r  42331  lclkr  42340  lclkrs  42346  hgmaprnlem2N  42704  hbtlem4  43886  hbtlem3  43887  itgoss  43923  omabs2  44092  naddgeoa  44154  naddwordnexlem4  44161  trrelind  44424  trrelsuperreldg  44427  trrelsuperrel2dg  44430  relexpss1d  44464  trclrelexplem  44470  relexpaddss  44477  frege97d  44511  frege109d  44516  frege131d  44523  clsk1indlem3  44802  limclner  46398  fourierdlem49  46902  fourierdlem92  46945  ovolval5lem3  47401  rhmsubcALTVlem4  49082  srhmsubcALTV  49123  fldhmsubcALTV  49131  rmsuppss  49183  scmsuppss  49184  imassc  49964  setrecsss  50512