Theorem 3sstr4d 3867

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

Syntax hints:   → wi 4   = wceq 1601   ⊆ wss 3792

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-in 3799  df-ss 3806

This theorem is referenced by:  suppimacnvss  7586  suppimacnv  7587  ressuppss  7595  suppun  7596  ressuppssdif  7597  suppfnss  7601  suppfnssOLD  7602  suppssov1  7609  suppssfv  7613  omwordri  7936  oewordri  7956  oaabs2  8009  fiss  8618  harword  8759  fin1a2lem12  9568  fzoss1  12814  fzoss2  12815  swrd0  13753  cshimadifsn  13980  trclfvss  14154  trclfvcotrg  14164  relexpnnrn  14192  vdwlem6  16094  vdwlem8  16096  hashbcss  16112  mrcss  16662  gsumzf1o  18699  gsumzaddlem  18707  dprdres  18814  dprdz  18816  dprdf1o  18818  mptscmfsupp0  19320  lspss  19379  lspsntrim  19493  aspss  19729  resspsrbas  19812  resspsradd  19813  resspsrmul  19814  clsss  21266  ntrss  21267  sslm  21511  1stcfb  21657  txss12  21817  prdstopn  21840  imasncls  21904  fmss  22158  flfssfcf  22250  cnpfcfi  22252  ressprdsds  22584  metss2lem  22724  metustto  22766  pi1addval  23255  pi1xfrcnv  23264  equivcau  23506  rrxmvallem  23610  uniiccvol  23784  dyaddisjlem  23799  volsup2  23809  itg2monolem1  23954  itg2gt0  23964  plyss  24392  lgamucov  25216  ifpsnprss  26970  wlkp1lem7  27030  occon  28718  spanss  28779  shlej1  28791  chscllem1  29068  chscllem2  29069  chscllem3  29070  ofrn2  30007  resf1o  30071  fpwrelmap  30074  orvclteinc  31136  dstfrvclim1  31138  reprss  31297  reprinfz1  31302  ss2mcls  32064  noetalem4  32455  heiborlem6  34239  lpssat  35167  lssat  35170  paddass  35992  pclssN  36048  2polssN  36069  polcon3N  36071  paddunN  36081  dibss  37323  dicssdvh  37340  dih2dimb  37398  dih2dimbALTN  37399  dihord5b  37413  dochss  37519  dochspss  37532  dvh3dim3N  37603  lclkrlem2r  37678  lclkr  37687  lclkrs  37693  hgmaprnlem2N  38051  hbtlem4  38655  hbtlem3  38656  itgoss  38692  trrelind  38914  trrelsuperreldg  38917  trrelsuperrel2dg  38920  relexpss1d  38954  trclrelexplem  38960  relexpaddss  38967  frege97d  39001  frege109d  39006  frege131d  39013  clsk1indlem3  39297  limclner  40791  fourierdlem49  41299  fourierdlem92  41342  rngchomfval  42981  rngccofval  42985  rnghmsscmap2  42988  rnghmsscmap  42989  ringchomfval  43027  ringccofval  43031  rhmsscmap2  43034  rhmsscmap  43035  rhmsscrnghm  43041  rngcresringcat  43045  srhmsubc  43091  fldhmsubc  43099  rhmsubclem3  43103  srhmsubcALTV  43109  fldhmsubcALTV  43117  rhmsubcALTVlem4  43122  rmsuppss  43166  mndpsuppss  43167  scmsuppss  43168  setrecsss  43552