Theorem 3sstr4d 3964

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

Syntax hints:   → wi 4   = wceq 1539   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  rescnvimafod  6933  suppimacnvss  7960  suppimacnv  7961  ressuppss  7970  suppun  7971  ressuppssdif  7972  suppfnss  7976  suppssov1  7985  suppssfv  7989  omwordri  8365  oewordri  8385  oaabs2  8439  fiss  9113  harword  9252  fin1a2lem12  10098  fzoss1  13342  fzoss2  13343  swrd0  14299  cshimadifsn  14470  trclfvss  14645  trclfvcotrg  14655  relexpnnrn  14684  vdwlem6  16615  vdwlem8  16617  hashbcss  16633  mrcss  17242  snsymgefmndeq  18917  gsumzf1o  19428  gsumzaddlem  19437  dprdres  19546  dprdz  19548  dprdf1o  19550  mptscmfsupp0  20103  lspss  20161  lspsntrim  20275  aspss  20991  resspsrbas  21094  resspsradd  21095  resspsrmul  21096  clsss  22113  ntrss  22114  sslm  22358  1stcfb  22504  txss12  22664  prdstopn  22687  imasncls  22751  fmss  23005  flfssfcf  23097  cnpfcfi  23099  ressprdsds  23432  metss2lem  23573  metustto  23615  pi1addval  24117  pi1xfrcnv  24126  equivcau  24369  rrxmvallem  24473  uniiccvol  24649  dyaddisjlem  24664  volsup2  24674  itg2monolem1  24820  itg2gt0  24830  plyss  25265  lgamucov  26092  ifpsnprss  27892  wlkp1lem7  27949  occon  29550  spanss  29611  shlej1  29623  chscllem1  29900  chscllem2  29901  chscllem3  29902  ofrn2  30878  resf1o  30967  fpwrelmap  30970  orvclteinc  32342  dstfrvclim1  32344  reprss  32497  reprinfz1  32502  revwlk  32986  ss2mcls  33430  naddssim  33764  madess  33986  heiborlem6  35901  lpssat  36954  lssat  36957  paddass  37779  pclssN  37835  2polssN  37856  polcon3N  37858  paddunN  37868  dibss  39110  dicssdvh  39127  dih2dimb  39185  dih2dimbALTN  39186  dihord5b  39200  dochss  39306  dochspss  39319  dvh3dim3N  39390  lclkrlem2r  39465  lclkr  39474  lclkrs  39480  hgmaprnlem2N  39838  hbtlem4  40867  hbtlem3  40868  itgoss  40904  trrelind  41162  trrelsuperreldg  41165  trrelsuperrel2dg  41168  relexpss1d  41202  trclrelexplem  41208  relexpaddss  41215  frege97d  41249  frege109d  41254  frege131d  41261  clsk1indlem3  41542  limclner  43082  fourierdlem49  43586  fourierdlem92  43629  rngchomfval  45412  rngccofval  45416  rnghmsscmap2  45419  rnghmsscmap  45420  ringchomfval  45458  ringccofval  45462  rhmsscmap2  45465  rhmsscmap  45466  rhmsscrnghm  45472  rngcresringcat  45476  srhmsubc  45522  fldhmsubc  45530  rhmsubclem3  45534  srhmsubcALTV  45540  fldhmsubcALTV  45548  rhmsubcALTVlem4  45553  rmsuppss  45594  mndpsuppss  45595  scmsuppss  45596  setrecsss  46292