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

Theorem eqimssi 3617
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 3582 . 2 𝐴𝐴
2 eqimssi.1 . 2 𝐴 = 𝐵
31, 2sseqtri 3595 1 𝐴𝐵
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474  wss 3535
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2592  df-cleq 2598  df-clel 2601  df-in 3542  df-ss 3549
This theorem is referenced by:  funi  5816  fpr  6300  tz7.48-2  7397  trcl  8460  zorn2lem4  9177  zmin  11612  elfzo1  12336  om2uzf1oi  12565  0trrel  13510  sumsplit  14283  isumless  14358  frlmip  19874  ust0  21771  rrxprds  22898  rrxip  22899  ovoliunnul  22995  vitalilem5  23100  logtayl  24119  mayetes3i  27774  eulerpartlemsv2  29549  eulerpartlemsv3  29552  eulerpartlemv  29555  eulerpartlemb  29559  poimirlem9  32387  dvasin  32465  cnvrcl0  36750  corclrcl  36817  trclrelexplem  36821  cotrcltrcl  36835  he0  36897  idhe  36900  dvsid  37351  binomcxplemnotnn0  37376  fourierdlem62  38861  fourierdlem66  38865  nbgr2vtx1edg  40570  nbuhgr2vtx1edgb  40572
  Copyright terms: Public domain W3C validator