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

Theorem 3sstr4d 3546
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 3532 . 2
51, 4mpbird 232 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  C_wss 3475
This theorem is referenced by:  suppimacnvss  6928  suppimacnv  6929  ressuppss  6938  suppun  6939  ressuppssdif  6940  suppfnss  6944  suppssov1  6951  suppssfv  6955  omwordri  7240  oewordri  7260  oaabs2  7313  fiss  7904  harword  8012  fin1a2lem12  8812  fzoss1  11852  fzoss2  11853  swrd0  12658  vdwlem6  14504  vdwlem8  14506  hashbcss  14522  mrcss  15013  gsumzf1o  16917  gsumzaddlem  16934  dprdres  17075  dprdz  17077  dprdf1o  17079  mptscmfsupp0  17576  lspss  17630  lspsntrim  17744  aspss  17981  resspsrbas  18070  resspsradd  18071  resspsrmul  18072  clsss  19555  ntrss  19556  sslm  19800  1stcfb  19946  txss12  20106  prdstopn  20129  imasncls  20193  fmss  20447  flfssfcf  20539  cnpfcfi  20541  ressprdsds  20874  metss2lem  21014  metusttoOLD  21060  metustto  21061  pi1addval  21548  pi1xfrcnv  21557  equivcau  21739  rrxmvallem  21831  uniiccvol  21989  dyaddisjlem  22004  volsup2  22014  itg2monolem1  22157  itg2gt0  22167  plyss  22596  occon  26205  spanss  26266  shlej1  26278  chscllem1  26555  chscllem2  26556  chscllem3  26557  ofrn2  27480  resf1o  27553  fpwrelmap  27556  orvclteinc  28414  dstfrvclim1  28416  lgamucov  28580  ss2mcls  28928  heiborlem6  30312  hbtlem4  31075  hbtlem3  31076  itgoss  31112  limclner  31657  fourierdlem49  31938  fourierdlem92  31981  rngchomfval  32774  rngccofval  32778  rnghmsscmap2  32781  rnghmsscmap  32782  ringchomfval  32820  ringccofval  32824  rhmsscmap2  32827  rhmsscmap  32828  rhmsscrnghm  32834  rngcresringcat  32838  srhmsubc  32884  fldhmsubc  32892  rhmsubclem3  32896  srhmsubcOLD  32903  fldhmsubcOLD  32911  rhmsubcOLDlem4  32916  rmsuppss  32963  mndpsuppss  32964  scmsuppss  32965  lpssat  34738  lssat  34741  paddass  35562  pclssN  35618  2polssN  35639  polcon3N  35641  paddunN  35651  dibss  36896  dicssdvh  36913  dih2dimb  36971  dih2dimbALTN  36972  dihord5b  36986  dochss  37092  dochspss  37105  dvh3dim3N  37176  lclkrlem2r  37251  lclkr  37260  lclkrs  37266  hgmaprnlem2N  37627  trrelind  37778  trrelsuperreldg  37783
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-in 3482  df-ss 3489
  Copyright terms: Public domain W3C validator