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

Theorem 3sstr4d 3393
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 3379 . 2  |-  ( ph  ->  ( C  C_  D  <->  A 
C_  B ) )
51, 4mpbird 225 1  |-  ( ph  ->  C  C_  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653    C_ wss 3322
This theorem is referenced by:  omwordri  6817  oewordri  6837  oaabs2  6890  fiss  7431  harword  7535  fin1a2lem12  8293  fzoss1  11164  fzoss2  11165  vdwlem6  13356  vdwlem8  13358  hashbcss  13374  mrcss  13843  dprdres  15588  dprdz  15590  dprdf1o  15592  lspss  16062  lspsntrim  16172  aspss  16393  resspsrbas  16480  resspsradd  16481  resspsrmul  16482  clsss  17120  ntrss  17121  sslm  17365  1stcfb  17510  txss12  17639  prdstopn  17662  imasncls  17726  fmss  17980  flfssfcf  18072  cnpfcfi  18074  ressprdsds  18403  metss2lem  18543  metusttoOLD  18589  metustto  18590  pi1addval  19075  pi1xfrcnv  19084  equivcau  19255  uniiccvol  19474  dyaddisjlem  19489  volsup2  19499  itg2monolem1  19644  itg2gt0  19654  plyss  20120  occon  22791  spanss  22852  shlej1  22864  chscllem1  23141  chscllem2  23142  chscllem3  23143  ofrn2  24055  orvclteinc  24735  dstfrvclim1  24737  lgamucov  24824  heiborlem6  26527  hbtlem4  27309  hbtlem3  27310  itgoss  27347  lpssat  29813  lssat  29816  paddass  30637  pclssN  30693  2polssN  30714  polcon3N  30716  paddunN  30726  dibss  31969  dicssdvh  31986  dih2dimb  32044  dih2dimbALTN  32045  dihord5b  32059  dochss  32165  dochspss  32178  dvh3dim3N  32249  lclkrlem2r  32324  lclkr  32333  lclkrs  32339  hgmaprnlem2N  32700
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-in 3329  df-ss 3336
  Copyright terms: Public domain W3C validator