MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3sstr4d Structured version   Visualization version   GIF version

Theorem 3sstr4d 4013
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
StepHypRef Expression
1 3sstr4d.1 . 2 (𝜑𝐴𝐵)
2 3sstr4d.2 . . 3 (𝜑𝐶 = 𝐴)
3 3sstr4d.3 . . 3 (𝜑𝐷 = 𝐵)
42, 3sseq12d 3999 . 2 (𝜑 → (𝐶𝐷𝐴𝐵))
51, 4mpbird 259 1 (𝜑𝐶𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1533  wss 3935
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3942  df-ss 3951
This theorem is referenced by:  suppimacnvss  7839  suppimacnv  7840  ressuppss  7848  suppun  7849  ressuppssdif  7850  suppfnss  7854  suppssov1  7861  suppssfv  7865  omwordri  8197  oewordri  8217  oaabs2  8271  fiss  8887  harword  9028  fin1a2lem12  9832  fzoss1  13063  fzoss2  13064  swrd0  14019  cshimadifsn  14190  trclfvss  14365  trclfvcotrg  14375  relexpnnrn  14403  vdwlem6  16321  vdwlem8  16323  hashbcss  16339  mrcss  16886  snsymgefmndeq  18522  gsumzf1o  19031  gsumzaddlem  19040  dprdres  19149  dprdz  19151  dprdf1o  19153  mptscmfsupp0  19698  lspss  19755  lspsntrim  19869  aspss  20105  resspsrbas  20194  resspsradd  20195  resspsrmul  20196  clsss  21661  ntrss  21662  sslm  21906  1stcfb  22052  txss12  22212  prdstopn  22235  imasncls  22299  fmss  22553  flfssfcf  22645  cnpfcfi  22647  ressprdsds  22980  metss2lem  23120  metustto  23162  pi1addval  23651  pi1xfrcnv  23660  equivcau  23902  rrxmvallem  24006  uniiccvol  24180  dyaddisjlem  24195  volsup2  24205  itg2monolem1  24350  itg2gt0  24360  plyss  24788  lgamucov  25614  ifpsnprss  27403  wlkp1lem7  27460  occon  29063  spanss  29124  shlej1  29136  chscllem1  29413  chscllem2  29414  chscllem3  29415  ofrn2  30386  resf1o  30465  fpwrelmap  30468  orvclteinc  31733  dstfrvclim1  31735  reprss  31888  reprinfz1  31893  revwlk  32371  ss2mcls  32815  noetalem4  33220  heiborlem6  35093  lpssat  36148  lssat  36151  paddass  36973  pclssN  37029  2polssN  37050  polcon3N  37052  paddunN  37062  dibss  38304  dicssdvh  38321  dih2dimb  38379  dih2dimbALTN  38380  dihord5b  38394  dochss  38500  dochspss  38513  dvh3dim3N  38584  lclkrlem2r  38659  lclkr  38668  lclkrs  38674  hgmaprnlem2N  39032  hbtlem4  39726  hbtlem3  39727  itgoss  39763  trrelind  40010  trrelsuperreldg  40013  trrelsuperrel2dg  40016  relexpss1d  40050  trclrelexplem  40056  relexpaddss  40063  frege97d  40097  frege109d  40102  frege131d  40109  clsk1indlem3  40393  limclner  41932  fourierdlem49  42441  fourierdlem92  42484  rngchomfval  44238  rngccofval  44242  rnghmsscmap2  44245  rnghmsscmap  44246  ringchomfval  44284  ringccofval  44288  rhmsscmap2  44291  rhmsscmap  44292  rhmsscrnghm  44298  rngcresringcat  44302  srhmsubc  44348  fldhmsubc  44356  rhmsubclem3  44360  srhmsubcALTV  44366  fldhmsubcALTV  44374  rhmsubcALTVlem4  44379  rmsuppss  44419  mndpsuppss  44420  scmsuppss  44421  setrecsss  44804
  Copyright terms: Public domain W3C validator