Theorem 3sstr4d 4042

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

Syntax hints:   → wi 4   = wceq 1536   ⊆ wss 3962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-ss 3979

This theorem is referenced by:  rescnvimafod  7092  suppimacnvss  8196  suppimacnv  8197  ressuppss  8206  suppun  8207  ressuppssdif  8208  suppfnss  8212  suppssov1  8220  suppssov2  8221  suppssfv  8225  omwordri  8608  oewordri  8628  oaabs2  8685  naddssim  8721  fiss  9461  harword  9600  fin1a2lem12  10448  fzoss1  13722  fzoss2  13723  swrd0  14692  cshimadifsn  14864  trclfvss  15041  trclfvcotrg  15051  relexpnnrn  15080  vdwlem6  17019  vdwlem8  17021  hashbcss  17037  mrcss  17660  mndpsuppss  18790  snsymgefmndeq  19426  gsumzf1o  19944  gsumzaddlem  19953  dprdres  20062  dprdz  20064  dprdf1o  20066  rngchomfval  20638  rngccofval  20642  rnghmsscmap2  20645  rnghmsscmap  20646  ringchomfval  20667  ringccofval  20671  rhmsscmap2  20674  rhmsscmap  20675  rhmsscrnghm  20681  rngcresringcat  20685  srhmsubc  20696  rhmsubclem3  20703  fldhmsubc  20802  mptscmfsupp0  20941  lspss  20999  lspsntrim  21114  aspss  21914  resspsrbas  22011  resspsradd  22012  resspsrmul  22013  clsss  23077  ntrss  23078  sslm  23322  1stcfb  23468  txss12  23628  prdstopn  23651  imasncls  23715  fmss  23969  flfssfcf  24061  cnpfcfi  24063  ressprdsds  24396  metss2lem  24539  metustto  24581  pi1addval  25094  pi1xfrcnv  25103  equivcau  25347  rrxmvallem  25451  uniiccvol  25628  dyaddisjlem  25643  volsup2  25653  itg2monolem1  25799  itg2gt0  25809  plyss  26252  lgamucov  27095  madess  27929  addsbday  28064  ifpsnprss  29655  wlkp1lem7  29711  occon  31315  spanss  31376  shlej1  31388  chscllem1  31665  chscllem2  31666  chscllem3  31667  ofrn2  32656  resf1o  32747  fpwrelmap  32750  ccatdmss  32918  fldgenss  33297  orvclteinc  34456  dstfrvclim1  34458  reprss  34610  reprinfz1  34615  revwlk  35108  ss2mcls  35552  heiborlem6  37802  lpssat  38994  lssat  38997  paddass  39820  pclssN  39876  2polssN  39897  polcon3N  39899  paddunN  39909  dibss  41151  dicssdvh  41168  dih2dimb  41226  dih2dimbALTN  41227  dihord5b  41241  dochss  41347  dochspss  41360  dvh3dim3N  41431  lclkrlem2r  41506  lclkr  41515  lclkrs  41521  hgmaprnlem2N  41879  hbtlem4  43114  hbtlem3  43115  itgoss  43151  omabs2  43321  naddgeoa  43383  naddwordnexlem4  43390  trrelind  43654  trrelsuperreldg  43657  trrelsuperrel2dg  43660  relexpss1d  43694  trclrelexplem  43700  relexpaddss  43707  frege97d  43741  frege109d  43746  frege131d  43753  clsk1indlem3  44032  limclner  45606  fourierdlem49  46110  fourierdlem92  46153  ovolval5lem3  46609  rhmsubcALTVlem4  48127  srhmsubcALTV  48168  fldhmsubcALTV  48176  rmsuppss  48214  scmsuppss  48215  setrecsss  48931