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

Theorem 3sstr4d 3532
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 3518 . 2  |-  ( ph  ->  ( C  C_  D  <->  A 
C_  B ) )
51, 4mpbird 232 1  |-  ( ph  ->  C  C_  D )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1398    C_ wss 3461
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-in 3468  df-ss 3475
This theorem is referenced by:  suppimacnvss  6901  suppimacnv  6902  ressuppss  6911  suppun  6912  ressuppssdif  6913  suppfnss  6917  suppssov1  6924  suppssfv  6928  omwordri  7213  oewordri  7233  oaabs2  7286  fiss  7876  harword  7983  fin1a2lem12  8782  fzoss1  11829  fzoss2  11830  swrd0  12650  trclfvss  12924  trclfvcotrg  12934  relexpnnrn  12960  vdwlem6  14588  vdwlem8  14590  hashbcss  14606  mrcss  15105  gsumzf1o  17116  gsumzaddlem  17133  dprdres  17270  dprdz  17272  dprdf1o  17274  mptscmfsupp0  17771  lspss  17825  lspsntrim  17939  aspss  18176  resspsrbas  18265  resspsradd  18266  resspsrmul  18267  clsss  19722  ntrss  19723  sslm  19967  1stcfb  20112  txss12  20272  prdstopn  20295  imasncls  20359  fmss  20613  flfssfcf  20705  cnpfcfi  20707  ressprdsds  21040  metss2lem  21180  metusttoOLD  21226  metustto  21227  pi1addval  21714  pi1xfrcnv  21723  equivcau  21905  rrxmvallem  21997  uniiccvol  22155  dyaddisjlem  22170  volsup2  22180  itg2monolem1  22323  itg2gt0  22333  plyss  22762  occon  26403  spanss  26464  shlej1  26476  chscllem1  26753  chscllem2  26754  chscllem3  26755  ofrn2  27701  resf1o  27784  fpwrelmap  27787  orvclteinc  28678  dstfrvclim1  28680  lgamucov  28844  ss2mcls  29192  heiborlem6  30552  hbtlem4  31316  hbtlem3  31317  itgoss  31353  limclner  31896  fourierdlem49  32177  fourierdlem92  32220  rngchomfval  33028  rngccofval  33032  rnghmsscmap2  33035  rnghmsscmap  33036  ringchomfval  33074  ringccofval  33078  rhmsscmap2  33081  rhmsscmap  33082  rhmsscrnghm  33088  rngcresringcat  33092  srhmsubc  33138  fldhmsubc  33146  rhmsubclem3  33150  srhmsubcALTV  33157  fldhmsubcALTV  33165  rhmsubcALTVlem4  33170  rmsuppss  33217  mndpsuppss  33218  scmsuppss  33219  lpssat  35135  lssat  35138  paddass  35959  pclssN  36015  2polssN  36036  polcon3N  36038  paddunN  36048  dibss  37293  dicssdvh  37310  dih2dimb  37368  dih2dimbALTN  37369  dihord5b  37383  dochss  37489  dochspss  37502  dvh3dim3N  37573  lclkrlem2r  37648  lclkr  37657  lclkrs  37663  hgmaprnlem2N  38024  trrelind  38185  trrelsuperreldg  38190  relexpaddss  38205  relexpss1d  38217  trclrelexplem  38229
  Copyright terms: Public domain W3C validator