Theorem 3sstr4d 4027

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.1	. 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2		3sstr4d.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐴)
3		3sstr4d.3	. . 3 ⊢ (𝜑 → 𝐷 = 𝐵)
4	2, 3	sseq12d 4013	. 2 ⊢ (𝜑 → (𝐶 ⊆ 𝐷 ↔ 𝐴 ⊆ 𝐵))
5	1, 4	mpbird 257	1 ⊢ (𝜑 → 𝐶 ⊆ 𝐷)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3953  df-ss 3963

This theorem is referenced by:  rescnvimafod  7070  suppimacnvss  8152  suppimacnv  8153  ressuppss  8162  suppun  8163  ressuppssdif  8164  suppfnss  8168  suppssov1  8177  suppssfv  8181  omwordri  8567  oewordri  8587  oaabs2  8643  naddssim  8679  fiss  9414  harword  9553  fin1a2lem12  10401  fzoss1  13654  fzoss2  13655  swrd0  14603  cshimadifsn  14775  trclfvss  14948  trclfvcotrg  14958  relexpnnrn  14987  vdwlem6  16914  vdwlem8  16916  hashbcss  16932  mrcss  17555  snsymgefmndeq  19254  gsumzf1o  19771  gsumzaddlem  19780  dprdres  19889  dprdz  19891  dprdf1o  19893  mptscmfsupp0  20524  lspss  20582  lspsntrim  20696  aspss  21412  resspsrbas  21516  resspsradd  21517  resspsrmul  21518  clsss  22539  ntrss  22540  sslm  22784  1stcfb  22930  txss12  23090  prdstopn  23113  imasncls  23177  fmss  23431  flfssfcf  23523  cnpfcfi  23525  ressprdsds  23858  metss2lem  24001  metustto  24043  pi1addval  24545  pi1xfrcnv  24554  equivcau  24798  rrxmvallem  24902  uniiccvol  25078  dyaddisjlem  25093  volsup2  25103  itg2monolem1  25249  itg2gt0  25259  plyss  25694  lgamucov  26521  madess  27350  ifpsnprss  28859  wlkp1lem7  28915  occon  30517  spanss  30578  shlej1  30590  chscllem1  30867  chscllem2  30868  chscllem3  30869  ofrn2  31842  resf1o  31932  fpwrelmap  31935  fldgenss  32374  orvclteinc  33411  dstfrvclim1  33413  reprss  33566  reprinfz1  33571  revwlk  34052  ss2mcls  34496  heiborlem6  36621  lpssat  37820  lssat  37823  paddass  38646  pclssN  38702  2polssN  38723  polcon3N  38725  paddunN  38735  dibss  39977  dicssdvh  39994  dih2dimb  40052  dih2dimbALTN  40053  dihord5b  40067  dochss  40173  dochspss  40186  dvh3dim3N  40257  lclkrlem2r  40332  lclkr  40341  lclkrs  40347  hgmaprnlem2N  40705  hbtlem4  41800  hbtlem3  41801  itgoss  41837  omabs2  42014  naddgeoa  42077  naddwordnexlem4  42084  trrelind  42348  trrelsuperreldg  42351  trrelsuperrel2dg  42354  relexpss1d  42388  trclrelexplem  42394  relexpaddss  42401  frege97d  42435  frege109d  42440  frege131d  42447  clsk1indlem3  42726  limclner  44301  fourierdlem49  44805  fourierdlem92  44848  ovolval5lem3  45304  rngchomfval  46765  rngccofval  46769  rnghmsscmap2  46772  rnghmsscmap  46773  ringchomfval  46811  ringccofval  46815  rhmsscmap2  46818  rhmsscmap  46819  rhmsscrnghm  46825  rngcresringcat  46829  srhmsubc  46875  fldhmsubc  46883  rhmsubclem3  46887  srhmsubcALTV  46893  fldhmsubcALTV  46901  rhmsubcALTVlem4  46906  rmsuppss  46947  mndpsuppss  46948  scmsuppss  46949  setrecsss  47647