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

Theorem 3sstr4d 3487
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  |-  ( ph  ->  A  C_  B )
3sstr4d.2  |-  ( ph  ->  C  =  A )
3sstr4d.3  |-  ( ph  ->  D  =  B )
Assertion
Ref Expression
3sstr4d  |-  ( ph  ->  C  C_  D )

Proof of Theorem 3sstr4d
StepHypRef Expression
1 3sstr4d.1 . 2  |-  ( ph  ->  A  C_  B )
2 3sstr4d.2 . . 3  |-  ( ph  ->  C  =  A )
3 3sstr4d.3 . . 3  |-  ( ph  ->  D  =  B )
42, 3sseq12d 3473 . 2  |-  ( ph  ->  ( C  C_  D  <->  A 
C_  B ) )
51, 4mpbird 240 1  |-  ( ph  ->  C  C_  D )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1455    C_ wss 3416
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-in 3423  df-ss 3430
This theorem is referenced by:  suppimacnvss  6956  suppimacnv  6957  ressuppss  6966  suppun  6967  ressuppssdif  6968  suppfnss  6972  suppssov1  6979  suppssfv  6983  omwordri  7304  oewordri  7324  oaabs2  7377  fiss  7969  harword  8111  fin1a2lem12  8872  fzoss1  11982  fzoss2  11983  swrd0  12833  trclfvss  13125  trclfvcotrg  13135  relexpnnrn  13163  vdwlem6  14991  vdwlem8  14993  hashbcss  15011  mrcss  15577  gsumzf1o  17601  gsumzaddlem  17609  dprdres  17716  dprdz  17718  dprdf1o  17720  mptscmfsupp0  18208  lspss  18262  lspsntrim  18376  aspss  18611  resspsrbas  18694  resspsradd  18695  resspsrmul  18696  clsss  20124  ntrss  20125  sslm  20370  1stcfb  20515  txss12  20675  prdstopn  20698  imasncls  20762  fmss  21016  flfssfcf  21108  cnpfcfi  21110  ressprdsds  21441  metss2lem  21581  metustto  21623  pi1addval  22134  pi1xfrcnv  22143  equivcau  22325  rrxmvallem  22413  uniiccvol  22593  dyaddisjlem  22609  volsup2  22619  itg2monolem1  22764  itg2gt0  22774  plyss  23209  lgamucov  24019  occon  26996  spanss  27057  shlej1  27069  chscllem1  27346  chscllem2  27347  chscllem3  27348  ofrn2  28294  resf1o  28367  fpwrelmap  28370  orvclteinc  29358  dstfrvclim1  29360  ss2mcls  30256  heiborlem6  32194  lpssat  32625  lssat  32628  paddass  33449  pclssN  33505  2polssN  33526  polcon3N  33528  paddunN  33538  dibss  34783  dicssdvh  34800  dih2dimb  34858  dih2dimbALTN  34859  dihord5b  34873  dochss  34979  dochspss  34992  dvh3dim3N  35063  lclkrlem2r  35138  lclkr  35147  lclkrs  35153  hgmaprnlem2N  35514  hbtlem4  36031  hbtlem3  36032  itgoss  36075  trrelind  36303  trrelsuperreldg  36306  trrelsuperrel2dg  36309  relexpss1d  36343  trclrelexplem  36349  relexpaddss  36356  frege97d  36390  frege109d  36395  frege131d  36402  limclner  37818  fourierdlem49  38120  fourierdlem92  38163  1wlkvtxeledg  39817  rngchomfval  40337  rngccofval  40341  rnghmsscmap2  40344  rnghmsscmap  40345  ringchomfval  40383  ringccofval  40387  rhmsscmap2  40390  rhmsscmap  40391  rhmsscrnghm  40397  rngcresringcat  40401  srhmsubc  40447  fldhmsubc  40455  rhmsubclem3  40459  srhmsubcALTV  40466  fldhmsubcALTV  40474  rhmsubcALTVlem4  40479  rmsuppss  40524  mndpsuppss  40525  scmsuppss  40526
  Copyright terms: Public domain W3C validator