MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqimssi Structured version   Visualization version   GIF version

Theorem eqimssi 4056
Description: Infer subclass relationship from equality. (Contributed by NM, 6-Jan-2007.)
Hypothesis
Ref Expression
eqimssi.1 𝐴 = 𝐵
Assertion
Ref Expression
eqimssi 𝐴𝐵

Proof of Theorem eqimssi
StepHypRef Expression
1 ssid 4018 . 2 𝐴𝐴
2 eqimssi.1 . 2 𝐴 = 𝐵
31, 2sseqtri 4032 1 𝐴𝐵
Colors of variables: wff setvar class
Syntax hints:   = wceq 1537  wss 3963
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727  df-ss 3980
This theorem is referenced by:  funi  6600  fpr  7174  tz7.48-2  8481  trcl  9766  zorn2lem4  10537  zmin  12984  elfzo1  13749  om2uzf1oi  13991  0trrel  15017  sumsplit  15801  isumless  15878  rnglidl1  21260  frlmip  21816  ust0  24244  rrxprds  25437  rrxip  25438  ovoliunnul  25556  vitalilem5  25661  logtayl  26717  nbgr2vtx1edg  29382  nbuhgr2vtx1edgb  29384  mayetes3i  31758  cycpmconjslem2  33158  eulerpartlemsv2  34340  eulerpartlemsv3  34343  eulerpartlemv  34346  eulerpartlemb  34350  poimirlem9  37616  dvasin  37691  dmcoss3  38435  disjALTVid  38737  sticksstones17  42145  sticksstones18  42146  nna4b4nsq  42647  cnvrcl0  43615  corclrcl  43697  trclrelexplem  43701  cotrcltrcl  43715  he0  43774  dvsid  44327  binomcxplemnotnn0  44352  fourierdlem62  46124  fourierdlem66  46128  isubgr3stgrlem6  47874
  Copyright terms: Public domain W3C validator