Theorem 3sstr4d 3963

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ⊆ wss 3895

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-ss 3896

This theorem is used by:  rescnvimafod  7074  suppimacnvss  8194  suppimacnv  8195  ressuppss  8204  suppun  8205  ressuppssdif  8206  suppfnss  8210  suppssov1  8218  suppssov2  8219  suppssfv  8223  omwordri  8584  oewordri  8605  oaabs2  8662  naddssim  8699  fiss  9420  harword  9561  rankval4b  9884  fin1a2lem12  10493  fzoss1  13825  fzoss2  13826  ccatdmss  14731  swrd0  14813  cshimadifsn  14985  trclfvss  15165  trclfvcotrg  15175  relexpnnrn  15204  vdwlem6  17170  vdwlem8  17172  hashbcss  17188  mrcss  17796  chnrev  18807  mndpsuppss  18965  snsymgefmndeq  19615  gsumzf1o  20132  gsumzaddlem  20141  dprdres  20250  dprdz  20252  dprdf1o  20254  rngchomfval  20880  rngccofval  20884  rnghmsscmap2  20887  rnghmsscmap  20888  ringchomfval  20909  ringccofval  20913  rhmsscmap2  20916  rhmsscmap  20917  rhmsscrnghm  20923  rngcresringcat  20927  srhmsubc  20938  rhmsubclem3  20945  fldhmsubc  21048  mptscmfsupp0  21208  lspss  21265  lspsntrim  21379  aspss  22190  resspsrbas  22287  resspsradd  22288  resspsrmul  22289  clsss  23378  ntrss  23379  sslm  23623  1stcfb  23769  txss12  23930  prdstopn  23953  imasncls  24017  fmss  24271  flfssfcf  24363  cnpfcfi  24365  ressprdsds  24696  metss2lem  24836  metustto  24878  pi1addval  25375  pi1xfrcnv  25384  equivcau  25627  rrxmvallem  25731  uniiccvol  25907  dyaddisjlem  25922  volsup2  25932  itg2monolem1  26077  itg2gt0  26087  plyss  26523  lgamucov  27371  madess  28258  oldss  28262  addbday  28410  ifpsnprss  30209  wlkp1lem7  30264  revwlk  30273  occon  31895  spanss  31956  shlej1  31968  chscllem1  32245  chscllem2  32246  chscllem3  32247  ofrn2  33282  resf1o  33369  fpwrelmap  33372  fldgenss  33925  orvclteinc  35155  dstfrvclim1  35157  reprss  35293  reprinfz1  35298  ss2mcls  36420  nmulss1  37056  heiborlem6  38844  lpssat  40164  lssat  40167  paddass  40989  pclssN  41045  2polssN  41066  polcon3N  41068  paddunN  41078  dibss  42320  dicssdvh  42337  dih2dimb  42395  dih2dimbALTN  42396  dihord5b  42410  dochss  42516  dochspss  42529  dvh3dim3N  42600  lclkrlem2r  42675  lclkr  42684  lclkrs  42690  hgmaprnlem2N  43048  hbtlem4  44222  hbtlem3  44223  itgoss  44259  omabs2  44428  naddgeoa  44490  naddwordnexlem4  44497  trrelind  44759  trrelsuperreldg  44762  trrelsuperrel2dg  44765  relexpss1d  44799  trclrelexplem  44805  relexpaddss  44812  frege97d  44846  frege109d  44851  frege131d  44858  clsk1indlem3  45137  limclner  46755  fourierdlem49  47259  fourierdlem92  47302  ovolval5lem3  47758  rhmsubcALTVlem4  49475  srhmsubcALTV  49516  fldhmsubcALTV  49524  rmsuppss  49576  scmsuppss  49577  imassc  50363  setrecsss  50963