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

Theorem eqimssi 3651
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 3616 . 2 𝐴𝐴
2 eqimssi.1 . 2 𝐴 = 𝐵
31, 2sseqtri 3629 1 𝐴𝐵
Colors of variables: wff setvar class
Syntax hints:   = wceq 1481  wss 3567
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-in 3574  df-ss 3581
This theorem is referenced by:  funi  5908  fpr  6406  tz7.48-2  7522  trcl  8589  zorn2lem4  9306  zmin  11769  elfzo1  12501  om2uzf1oi  12735  0trrel  13701  sumsplit  14480  isumless  14558  frlmip  20098  ust0  22004  rrxprds  23158  rrxip  23159  ovoliunnul  23256  vitalilem5  23362  logtayl  24387  nbgr2vtx1edg  26227  nbuhgr2vtx1edgb  26229  mayetes3i  28558  eulerpartlemsv2  30394  eulerpartlemsv3  30397  eulerpartlemv  30400  eulerpartlemb  30404  poimirlem9  33389  dvasin  33467  cnvrcl0  37751  corclrcl  37818  trclrelexplem  37822  cotrcltrcl  37836  he0  37898  idhe  37901  dvsid  38350  binomcxplemnotnn0  38375  fourierdlem62  40148  fourierdlem66  40152
  Copyright terms: Public domain W3C validator