Theorem 3sstr4d 3962

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

Syntax hints:   → wi 4   = wceq 1538   ⊆ wss 3881

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898

This theorem is referenced by:  suppimacnvss  7823  suppimacnv  7824  ressuppss  7832  suppun  7833  ressuppssdif  7834  suppfnss  7838  suppssov1  7845  suppssfv  7849  omwordri  8181  oewordri  8201  oaabs2  8255  fiss  8872  harword  9011  fin1a2lem12  9822  fzoss1  13059  fzoss2  13060  swrd0  14011  cshimadifsn  14182  trclfvss  14357  trclfvcotrg  14367  relexpnnrn  14396  vdwlem6  16312  vdwlem8  16314  hashbcss  16330  mrcss  16879  snsymgefmndeq  18515  gsumzf1o  19025  gsumzaddlem  19034  dprdres  19143  dprdz  19145  dprdf1o  19147  mptscmfsupp0  19692  lspss  19749  lspsntrim  19863  aspss  20563  resspsrbas  20653  resspsradd  20654  resspsrmul  20655  clsss  21659  ntrss  21660  sslm  21904  1stcfb  22050  txss12  22210  prdstopn  22233  imasncls  22297  fmss  22551  flfssfcf  22643  cnpfcfi  22645  ressprdsds  22978  metss2lem  23118  metustto  23160  pi1addval  23653  pi1xfrcnv  23662  equivcau  23904  rrxmvallem  24008  uniiccvol  24184  dyaddisjlem  24199  volsup2  24209  itg2monolem1  24354  itg2gt0  24364  plyss  24796  lgamucov  25623  ifpsnprss  27412  wlkp1lem7  27469  occon  29070  spanss  29131  shlej1  29143  chscllem1  29420  chscllem2  29421  chscllem3  29422  ofrn2  30401  resf1o  30492  fpwrelmap  30495  orvclteinc  31843  dstfrvclim1  31845  reprss  31998  reprinfz1  32003  revwlk  32484  ss2mcls  32928  noetalem4  33333  heiborlem6  35254  lpssat  36309  lssat  36312  paddass  37134  pclssN  37190  2polssN  37211  polcon3N  37213  paddunN  37223  dibss  38465  dicssdvh  38482  dih2dimb  38540  dih2dimbALTN  38541  dihord5b  38555  dochss  38661  dochspss  38674  dvh3dim3N  38745  lclkrlem2r  38820  lclkr  38829  lclkrs  38835  hgmaprnlem2N  39193  hbtlem4  40070  hbtlem3  40071  itgoss  40107  trrelind  40366  trrelsuperreldg  40369  trrelsuperrel2dg  40372  relexpss1d  40406  trclrelexplem  40412  relexpaddss  40419  frege97d  40453  frege109d  40458  frege131d  40465  clsk1indlem3  40746  limclner  42293  fourierdlem49  42797  fourierdlem92  42840  rngchomfval  44590  rngccofval  44594  rnghmsscmap2  44597  rnghmsscmap  44598  ringchomfval  44636  ringccofval  44640  rhmsscmap2  44643  rhmsscmap  44644  rhmsscrnghm  44650  rngcresringcat  44654  srhmsubc  44700  fldhmsubc  44708  rhmsubclem3  44712  srhmsubcALTV  44718  fldhmsubcALTV  44726  rhmsubcALTVlem4  44731  rmsuppss  44772  mndpsuppss  44773  scmsuppss  44774  setrecsss  45230