Theorem 3sstr4d 3977

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.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐴)
2		3sstr4d.1	. . 3 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
3	1, 2	eqsstrd 3956	. 2 ⊢ (𝜑 → 𝐶 ⊆ 𝐵)
4		3sstr4d.3	. 2 ⊢ (𝜑 → 𝐷 = 𝐵)
5	3, 4	sseqtrrd 3959	1 ⊢ (𝜑 → 𝐶 ⊆ 𝐷)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-ss 3906

This theorem is referenced by:  rescnvimafod  7025  suppimacnvss  8123  suppimacnv  8124  ressuppss  8133  suppun  8134  ressuppssdif  8135  suppfnss  8139  suppssov1  8147  suppssov2  8148  suppssfv  8152  omwordri  8507  oewordri  8528  oaabs2  8585  naddssim  8621  fiss  9337  harword  9478  fin1a2lem12  10333  fzoss1  13641  fzoss2  13642  ccatdmss  14544  swrd0  14621  cshimadifsn  14791  trclfvss  14968  trclfvcotrg  14978  relexpnnrn  15007  vdwlem6  16957  vdwlem8  16959  hashbcss  16975  mrcss  17582  chnrev  18593  mndpsuppss  18733  snsymgefmndeq  19370  gsumzf1o  19887  gsumzaddlem  19896  dprdres  20005  dprdz  20007  dprdf1o  20009  rngchomfval  20599  rngccofval  20603  rnghmsscmap2  20606  rnghmsscmap  20607  ringchomfval  20628  ringccofval  20632  rhmsscmap2  20635  rhmsscmap  20636  rhmsscrnghm  20642  rngcresringcat  20646  srhmsubc  20657  rhmsubclem3  20664  fldhmsubc  20762  mptscmfsupp0  20922  lspss  20979  lspsntrim  21093  aspss  21856  resspsrbas  21952  resspsradd  21953  resspsrmul  21954  clsss  23019  ntrss  23020  sslm  23264  1stcfb  23410  txss12  23570  prdstopn  23593  imasncls  23657  fmss  23911  flfssfcf  24003  cnpfcfi  24005  ressprdsds  24336  metss2lem  24476  metustto  24518  pi1addval  25015  pi1xfrcnv  25024  equivcau  25267  rrxmvallem  25371  uniiccvol  25547  dyaddisjlem  25562  volsup2  25572  itg2monolem1  25717  itg2gt0  25727  plyss  26164  lgamucov  27001  madess  27858  oldss  27862  addbday  28010  ifpsnprss  29691  wlkp1lem7  29746  occon  31358  spanss  31419  shlej1  31431  chscllem1  31708  chscllem2  31709  chscllem3  31710  ofrn2  32713  resf1o  32803  fpwrelmap  32806  fldgenss  33377  orvclteinc  34620  dstfrvclim1  34622  reprss  34761  reprinfz1  34766  rankval4b  35243  revwlk  35307  ss2mcls  35750  heiborlem6  38137  lpssat  39459  lssat  39462  paddass  40284  pclssN  40340  2polssN  40361  polcon3N  40363  paddunN  40373  dibss  41615  dicssdvh  41632  dih2dimb  41690  dih2dimbALTN  41691  dihord5b  41705  dochss  41811  dochspss  41824  dvh3dim3N  41895  lclkrlem2r  41970  lclkr  41979  lclkrs  41985  hgmaprnlem2N  42343  hbtlem4  43554  hbtlem3  43555  itgoss  43591  omabs2  43760  naddgeoa  43822  naddwordnexlem4  43829  trrelind  44092  trrelsuperreldg  44095  trrelsuperrel2dg  44098  relexpss1d  44132  trclrelexplem  44138  relexpaddss  44145  frege97d  44179  frege109d  44184  frege131d  44191  clsk1indlem3  44470  limclner  46079  fourierdlem49  46583  fourierdlem92  46626  ovolval5lem3  47082  rhmsubcALTVlem4  48760  srhmsubcALTV  48801  fldhmsubcALTV  48809  rmsuppss  48846  scmsuppss  48847  imassc  49628  setrecsss  50176