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

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

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 2705

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

This theorem is referenced by:  rescnvimafod  7014  suppimacnvss  8111  suppimacnv  8112  ressuppss  8121  suppun  8122  ressuppssdif  8123  suppfnss  8127  suppssov1  8135  suppssov2  8136  suppssfv  8140  omwordri  8495  oewordri  8515  oaabs2  8572  naddssim  8608  fiss  9317  harword  9458  fin1a2lem12  10311  fzoss1  13590  fzoss2  13591  ccatdmss  14493  swrd0  14570  cshimadifsn  14740  trclfvss  14917  trclfvcotrg  14927  relexpnnrn  14956  vdwlem6  16902  vdwlem8  16904  hashbcss  16920  mrcss  17526  chnrev  18537  mndpsuppss  18677  snsymgefmndeq  19311  gsumzf1o  19828  gsumzaddlem  19837  dprdres  19946  dprdz  19948  dprdf1o  19950  rngchomfval  20541  rngccofval  20545  rnghmsscmap2  20548  rnghmsscmap  20549  ringchomfval  20570  ringccofval  20574  rhmsscmap2  20577  rhmsscmap  20578  rhmsscrnghm  20584  rngcresringcat  20588  srhmsubc  20599  rhmsubclem3  20606  fldhmsubc  20704  mptscmfsupp0  20864  lspss  20921  lspsntrim  21036  aspss  21818  resspsrbas  21914  resspsradd  21915  resspsrmul  21916  clsss  22972  ntrss  22973  sslm  23217  1stcfb  23363  txss12  23523  prdstopn  23546  imasncls  23610  fmss  23864  flfssfcf  23956  cnpfcfi  23958  ressprdsds  24289  metss2lem  24429  metustto  24471  pi1addval  24978  pi1xfrcnv  24987  equivcau  25230  rrxmvallem  25334  uniiccvol  25511  dyaddisjlem  25526  volsup2  25536  itg2monolem1  25681  itg2gt0  25691  plyss  26134  lgamucov  26978  madess  27824  oldss  27826  addsbday  27963  ifpsnprss  29605  wlkp1lem7  29660  occon  31271  spanss  31332  shlej1  31344  chscllem1  31621  chscllem2  31622  chscllem3  31623  ofrn2  32626  resf1o  32719  fpwrelmap  32722  fldgenss  33291  orvclteinc  34512  dstfrvclim1  34514  reprss  34653  reprinfz1  34658  rankval4b  35134  revwlk  35192  ss2mcls  35635  heiborlem6  37879  lpssat  39135  lssat  39138  paddass  39960  pclssN  40016  2polssN  40037  polcon3N  40039  paddunN  40049  dibss  41291  dicssdvh  41308  dih2dimb  41366  dih2dimbALTN  41367  dihord5b  41381  dochss  41487  dochspss  41500  dvh3dim3N  41571  lclkrlem2r  41646  lclkr  41655  lclkrs  41661  hgmaprnlem2N  42019  hbtlem4  43246  hbtlem3  43247  itgoss  43283  omabs2  43452  naddgeoa  43514  naddwordnexlem4  43521  trrelind  43785  trrelsuperreldg  43788  trrelsuperrel2dg  43791  relexpss1d  43825  trclrelexplem  43831  relexpaddss  43838  frege97d  43872  frege109d  43877  frege131d  43884  clsk1indlem3  44163  limclner  45776  fourierdlem49  46280  fourierdlem92  46323  ovolval5lem3  46779  rhmsubcALTVlem4  48411  srhmsubcALTV  48452  fldhmsubcALTV  48460  rmsuppss  48497  scmsuppss  48498  imassc  49281  setrecsss  49829