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

Theorem 3sstr3d 3233
Description: Substitution of equality into both sides of a subclass relationship. (Contributed by NM, 1-Oct-2000.)
Hypotheses
Ref Expression
3sstr3d.1  |-  ( ph  ->  A  C_  B )
3sstr3d.2  |-  ( ph  ->  A  =  C )
3sstr3d.3  |-  ( ph  ->  B  =  D )
Assertion
Ref Expression
3sstr3d  |-  ( ph  ->  C  C_  D )

Proof of Theorem 3sstr3d
StepHypRef Expression
1 3sstr3d.1 . 2  |-  ( ph  ->  A  C_  B )
2 3sstr3d.2 . . 3  |-  ( ph  ->  A  =  C )
3 3sstr3d.3 . . 3  |-  ( ph  ->  B  =  D )
42, 3sseq12d 3220 . 2  |-  ( ph  ->  ( A  C_  B  <->  C 
C_  D ) )
51, 4mpbid 201 1  |-  ( ph  ->  C  C_  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632    C_ wss 3165
This theorem is referenced by:  cnvtsr  14347  dprdss  15280  dprd2da  15293  dmdprdsplit2lem  15296  mplind  16259  txcmplem1  17351  setsmstopn  18040  tngtopn  18182  bcthlem2  18763  bcthlem4  18765  uniiccvol  18951  dyadmaxlem  18968  dvlip2  19358  dvne0  19374  shlej2  21956  bnd2lem  26618  heiborlem8  26645  hbtlem5  27435  dochord  32182  lclkrlem2p  32334  mapdsn  32453
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator