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

Theorem 3sstr3d 3390
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 3377 . 2  |-  ( ph  ->  ( A  C_  B  <->  C 
C_  D ) )
51, 4mpbid 202 1  |-  ( ph  ->  C  C_  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652    C_ wss 3320
This theorem is referenced by:  cnvtsr  14654  dprdss  15587  dprd2da  15600  dmdprdsplit2lem  15603  mplind  16562  txcmplem1  17673  setsmstopn  18508  tngtopn  18691  bcthlem2  19278  bcthlem4  19280  uniiccvol  19472  dyadmaxlem  19489  dvlip2  19879  dvne0  19895  shlej2  22863  hauseqcn  24293  bnd2lem  26500  heiborlem8  26527  hbtlem5  27309  dochord  32168  lclkrlem2p  32320  mapdsn  32439
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-in 3327  df-ss 3334
  Copyright terms: Public domain W3C validator