Theorem 3sstr4d 3991

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

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

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 3920

This theorem is referenced by:  rescnvimafod  7027  suppimacnvss  8125  suppimacnv  8126  ressuppss  8135  suppun  8136  ressuppssdif  8137  suppfnss  8141  suppssov1  8149  suppssov2  8150  suppssfv  8154  omwordri  8509  oewordri  8530  oaabs2  8587  naddssim  8623  fiss  9339  harword  9480  fin1a2lem12  10333  fzoss1  13614  fzoss2  13615  ccatdmss  14517  swrd0  14594  cshimadifsn  14764  trclfvss  14941  trclfvcotrg  14951  relexpnnrn  14980  vdwlem6  16926  vdwlem8  16928  hashbcss  16944  mrcss  17551  chnrev  18562  mndpsuppss  18702  snsymgefmndeq  19336  gsumzf1o  19853  gsumzaddlem  19862  dprdres  19971  dprdz  19973  dprdf1o  19975  rngchomfval  20567  rngccofval  20571  rnghmsscmap2  20574  rnghmsscmap  20575  ringchomfval  20596  ringccofval  20600  rhmsscmap2  20603  rhmsscmap  20604  rhmsscrnghm  20610  rngcresringcat  20614  srhmsubc  20625  rhmsubclem3  20632  fldhmsubc  20730  mptscmfsupp0  20890  lspss  20947  lspsntrim  21062  aspss  21844  resspsrbas  21941  resspsradd  21942  resspsrmul  21943  clsss  23010  ntrss  23011  sslm  23255  1stcfb  23401  txss12  23561  prdstopn  23584  imasncls  23648  fmss  23902  flfssfcf  23994  cnpfcfi  23996  ressprdsds  24327  metss2lem  24467  metustto  24509  pi1addval  25016  pi1xfrcnv  25025  equivcau  25268  rrxmvallem  25372  uniiccvol  25549  dyaddisjlem  25564  volsup2  25574  itg2monolem1  25719  itg2gt0  25729  plyss  26172  lgamucov  27016  madess  27874  oldss  27878  addbday  28026  ifpsnprss  29708  wlkp1lem7  29763  occon  31374  spanss  31435  shlej1  31447  chscllem1  31724  chscllem2  31725  chscllem3  31726  ofrn2  32729  resf1o  32819  fpwrelmap  32822  fldgenss  33409  orvclteinc  34653  dstfrvclim1  34655  reprss  34794  reprinfz1  34799  rankval4b  35275  revwlk  35338  ss2mcls  35781  heiborlem6  38064  lpssat  39386  lssat  39389  paddass  40211  pclssN  40267  2polssN  40288  polcon3N  40290  paddunN  40300  dibss  41542  dicssdvh  41559  dih2dimb  41617  dih2dimbALTN  41618  dihord5b  41632  dochss  41738  dochspss  41751  dvh3dim3N  41822  lclkrlem2r  41897  lclkr  41906  lclkrs  41912  hgmaprnlem2N  42270  hbtlem4  43480  hbtlem3  43481  itgoss  43517  omabs2  43686  naddgeoa  43748  naddwordnexlem4  43755  trrelind  44018  trrelsuperreldg  44021  trrelsuperrel2dg  44024  relexpss1d  44058  trclrelexplem  44064  relexpaddss  44071  frege97d  44105  frege109d  44110  frege131d  44117  clsk1indlem3  44396  limclner  46006  fourierdlem49  46510  fourierdlem92  46553  ovolval5lem3  47009  rhmsubcALTVlem4  48641  srhmsubcALTV  48682  fldhmsubcALTV  48690  rmsuppss  48727  scmsuppss  48728  imassc  49509  setrecsss  50057