Theorem 3sstr4d 4056

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

Syntax hints:   → wi 4   = wceq 1537   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ss 3993

This theorem is referenced by:  rescnvimafod  7107  suppimacnvss  8214  suppimacnv  8215  ressuppss  8224  suppun  8225  ressuppssdif  8226  suppfnss  8230  suppssov1  8238  suppssov2  8239  suppssfv  8243  omwordri  8628  oewordri  8648  oaabs2  8705  naddssim  8741  fiss  9493  harword  9632  fin1a2lem12  10480  fzoss1  13743  fzoss2  13744  swrd0  14706  cshimadifsn  14878  trclfvss  15055  trclfvcotrg  15065  relexpnnrn  15094  vdwlem6  17033  vdwlem8  17035  hashbcss  17051  mrcss  17674  snsymgefmndeq  19436  gsumzf1o  19954  gsumzaddlem  19963  dprdres  20072  dprdz  20074  dprdf1o  20076  rngchomfval  20644  rngccofval  20648  rnghmsscmap2  20651  rnghmsscmap  20652  ringchomfval  20673  ringccofval  20677  rhmsscmap2  20680  rhmsscmap  20681  rhmsscrnghm  20687  rngcresringcat  20691  srhmsubc  20702  rhmsubclem3  20709  fldhmsubc  20808  mptscmfsupp0  20947  lspss  21005  lspsntrim  21120  aspss  21920  resspsrbas  22017  resspsradd  22018  resspsrmul  22019  clsss  23083  ntrss  23084  sslm  23328  1stcfb  23474  txss12  23634  prdstopn  23657  imasncls  23721  fmss  23975  flfssfcf  24067  cnpfcfi  24069  ressprdsds  24402  metss2lem  24545  metustto  24587  pi1addval  25100  pi1xfrcnv  25109  equivcau  25353  rrxmvallem  25457  uniiccvol  25634  dyaddisjlem  25649  volsup2  25659  itg2monolem1  25805  itg2gt0  25815  plyss  26258  lgamucov  27099  madess  27933  addsbday  28068  ifpsnprss  29659  wlkp1lem7  29715  occon  31319  spanss  31380  shlej1  31392  chscllem1  31669  chscllem2  31670  chscllem3  31671  ofrn2  32659  resf1o  32744  fpwrelmap  32747  ccatdmss  32916  fldgenss  33283  orvclteinc  34440  dstfrvclim1  34442  reprss  34594  reprinfz1  34599  revwlk  35092  ss2mcls  35536  heiborlem6  37776  lpssat  38969  lssat  38972  paddass  39795  pclssN  39851  2polssN  39872  polcon3N  39874  paddunN  39884  dibss  41126  dicssdvh  41143  dih2dimb  41201  dih2dimbALTN  41202  dihord5b  41216  dochss  41322  dochspss  41335  dvh3dim3N  41406  lclkrlem2r  41481  lclkr  41490  lclkrs  41496  hgmaprnlem2N  41854  hbtlem4  43083  hbtlem3  43084  itgoss  43120  omabs2  43294  naddgeoa  43356  naddwordnexlem4  43363  trrelind  43627  trrelsuperreldg  43630  trrelsuperrel2dg  43633  relexpss1d  43667  trclrelexplem  43673  relexpaddss  43680  frege97d  43714  frege109d  43719  frege131d  43726  clsk1indlem3  44005  limclner  45572  fourierdlem49  46076  fourierdlem92  46119  ovolval5lem3  46575  rhmsubcALTVlem4  48007  srhmsubcALTV  48048  fldhmsubcALTV  48056  rmsuppss  48095  mndpsuppss  48096  scmsuppss  48097  setrecsss  48793