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

Theorem 3sstr3d 3545
Description: Substitution of equality into both sides of a subclass relationship. (Contributed by NM, 1-Oct-2000.)
Hypotheses
Ref Expression
3sstr3d.1
3sstr3d.2
3sstr3d.3
Assertion
Ref Expression
3sstr3d

Proof of Theorem 3sstr3d
StepHypRef Expression
1 3sstr3d.1 . 2
2 3sstr3d.2 . . 3
3 3sstr3d.3 . . 3
42, 3sseq12d 3532 . 2
51, 4mpbid 210 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  C_wss 3475
This theorem is referenced by:  cnvtsr  15852  dprdss  17076  dprd2da  17091  dmdprdsplit2lem  17094  mplind  18167  txcmplem1  20142  setsmstopn  20981  tngtopn  21164  bcthlem2  21764  bcthlem4  21766  uniiccvol  21989  dyadmaxlem  22006  dvlip2  22396  dvne0  22412  shlej2  26279  hauseqcn  27877  bnd2lem  30287  heiborlem8  30314  hbtlem5  31077  dochord  37097  lclkrlem2p  37249  mapdsn  37368
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-in 3482  df-ss 3489
  Copyright terms: Public domain W3C validator