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

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3922

This theorem is referenced by:  rescnvimafod  7011  suppimacnvss  8113  suppimacnv  8114  ressuppss  8123  suppun  8124  ressuppssdif  8125  suppfnss  8129  suppssov1  8137  suppssov2  8138  suppssfv  8142  omwordri  8497  oewordri  8517  oaabs2  8574  naddssim  8610  fiss  9333  harword  9474  fin1a2lem12  10324  fzoss1  13607  fzoss2  13608  swrd0  14583  cshimadifsn  14754  trclfvss  14931  trclfvcotrg  14941  relexpnnrn  14970  vdwlem6  16916  vdwlem8  16918  hashbcss  16934  mrcss  17540  mndpsuppss  18657  snsymgefmndeq  19292  gsumzf1o  19809  gsumzaddlem  19818  dprdres  19927  dprdz  19929  dprdf1o  19931  rngchomfval  20525  rngccofval  20529  rnghmsscmap2  20532  rnghmsscmap  20533  ringchomfval  20554  ringccofval  20558  rhmsscmap2  20561  rhmsscmap  20562  rhmsscrnghm  20568  rngcresringcat  20572  srhmsubc  20583  rhmsubclem3  20590  fldhmsubc  20688  mptscmfsupp0  20848  lspss  20905  lspsntrim  21020  aspss  21802  resspsrbas  21899  resspsradd  21900  resspsrmul  21901  clsss  22957  ntrss  22958  sslm  23202  1stcfb  23348  txss12  23508  prdstopn  23531  imasncls  23595  fmss  23849  flfssfcf  23941  cnpfcfi  23943  ressprdsds  24275  metss2lem  24415  metustto  24457  pi1addval  24964  pi1xfrcnv  24973  equivcau  25216  rrxmvallem  25320  uniiccvol  25497  dyaddisjlem  25512  volsup2  25522  itg2monolem1  25667  itg2gt0  25677  plyss  26120  lgamucov  26964  madess  27808  oldss  27810  addsbday  27947  ifpsnprss  29586  wlkp1lem7  29641  occon  31249  spanss  31310  shlej1  31322  chscllem1  31599  chscllem2  31600  chscllem3  31601  ofrn2  32597  resf1o  32686  fpwrelmap  32689  ccatdmss  32904  fldgenss  33268  orvclteinc  34446  dstfrvclim1  34448  reprss  34587  reprinfz1  34592  revwlk  35100  ss2mcls  35543  heiborlem6  37798  lpssat  38994  lssat  38997  paddass  39820  pclssN  39876  2polssN  39897  polcon3N  39899  paddunN  39909  dibss  41151  dicssdvh  41168  dih2dimb  41226  dih2dimbALTN  41227  dihord5b  41241  dochss  41347  dochspss  41360  dvh3dim3N  41431  lclkrlem2r  41506  lclkr  41515  lclkrs  41521  hgmaprnlem2N  41879  hbtlem4  43102  hbtlem3  43103  itgoss  43139  omabs2  43308  naddgeoa  43370  naddwordnexlem4  43377  trrelind  43641  trrelsuperreldg  43644  trrelsuperrel2dg  43647  relexpss1d  43681  trclrelexplem  43687  relexpaddss  43694  frege97d  43728  frege109d  43733  frege131d  43740  clsk1indlem3  44019  limclner  45636  fourierdlem49  46140  fourierdlem92  46183  ovolval5lem3  46639  rhmsubcALTVlem4  48272  srhmsubcALTV  48313  fldhmsubcALTV  48321  rmsuppss  48358  scmsuppss  48359  imassc  49142  setrecsss  49690