Theorem 3sstr4d 4030

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

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

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 3956  df-ss 3966

This theorem is referenced by:  rescnvimafod  7076  suppimacnvss  8158  suppimacnv  8159  ressuppss  8168  suppun  8169  ressuppssdif  8170  suppfnss  8174  suppssov1  8183  suppssfv  8187  omwordri  8572  oewordri  8592  oaabs2  8648  naddssim  8684  fiss  9419  harword  9558  fin1a2lem12  10406  fzoss1  13659  fzoss2  13660  swrd0  14608  cshimadifsn  14780  trclfvss  14953  trclfvcotrg  14963  relexpnnrn  14992  vdwlem6  16919  vdwlem8  16921  hashbcss  16937  mrcss  17560  snsymgefmndeq  19262  gsumzf1o  19780  gsumzaddlem  19789  dprdres  19898  dprdz  19900  dprdf1o  19902  mptscmfsupp0  20537  lspss  20595  lspsntrim  20709  aspss  21431  resspsrbas  21535  resspsradd  21536  resspsrmul  21537  clsss  22558  ntrss  22559  sslm  22803  1stcfb  22949  txss12  23109  prdstopn  23132  imasncls  23196  fmss  23450  flfssfcf  23542  cnpfcfi  23544  ressprdsds  23877  metss2lem  24020  metustto  24062  pi1addval  24564  pi1xfrcnv  24573  equivcau  24817  rrxmvallem  24921  uniiccvol  25097  dyaddisjlem  25112  volsup2  25122  itg2monolem1  25268  itg2gt0  25278  plyss  25713  lgamucov  26542  madess  27371  ifpsnprss  28880  wlkp1lem7  28936  occon  30540  spanss  30601  shlej1  30613  chscllem1  30890  chscllem2  30891  chscllem3  30892  ofrn2  31865  resf1o  31955  fpwrelmap  31958  fldgenss  32406  orvclteinc  33474  dstfrvclim1  33476  reprss  33629  reprinfz1  33634  revwlk  34115  ss2mcls  34559  heiborlem6  36684  lpssat  37883  lssat  37886  paddass  38709  pclssN  38765  2polssN  38786  polcon3N  38788  paddunN  38798  dibss  40040  dicssdvh  40057  dih2dimb  40115  dih2dimbALTN  40116  dihord5b  40130  dochss  40236  dochspss  40249  dvh3dim3N  40320  lclkrlem2r  40395  lclkr  40404  lclkrs  40410  hgmaprnlem2N  40768  hbtlem4  41868  hbtlem3  41869  itgoss  41905  omabs2  42082  naddgeoa  42145  naddwordnexlem4  42152  trrelind  42416  trrelsuperreldg  42419  trrelsuperrel2dg  42422  relexpss1d  42456  trclrelexplem  42462  relexpaddss  42469  frege97d  42503  frege109d  42508  frege131d  42515  clsk1indlem3  42794  limclner  44367  fourierdlem49  44871  fourierdlem92  44914  ovolval5lem3  45370  rngchomfval  46864  rngccofval  46868  rnghmsscmap2  46871  rnghmsscmap  46872  ringchomfval  46910  ringccofval  46914  rhmsscmap2  46917  rhmsscmap  46918  rhmsscrnghm  46924  rngcresringcat  46928  srhmsubc  46974  fldhmsubc  46982  rhmsubclem3  46986  srhmsubcALTV  46992  fldhmsubcALTV  47000  rhmsubcALTVlem4  47005  rmsuppss  47046  mndpsuppss  47047  scmsuppss  47048  setrecsss  47746