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

Theorem eqimssi 3622
 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 3587 . 2 𝐴𝐴
2 eqimssi.1 . 2 𝐴 = 𝐵
31, 2sseqtri 3600 1 𝐴𝐵
 Colors of variables: wff setvar class Syntax hints:   = wceq 1475   ⊆ wss 3540 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554 This theorem is referenced by:  funi  5834  fpr  6326  tz7.48-2  7424  trcl  8487  zorn2lem4  9204  zmin  11660  elfzo1  12385  om2uzf1oi  12614  0trrel  13568  sumsplit  14341  isumless  14416  frlmip  19936  ust0  21833  rrxprds  22985  rrxip  22986  ovoliunnul  23082  vitalilem5  23187  logtayl  24206  mayetes3i  27972  eulerpartlemsv2  29747  eulerpartlemsv3  29750  eulerpartlemv  29753  eulerpartlemb  29757  poimirlem9  32588  dvasin  32666  cnvrcl0  36951  corclrcl  37018  trclrelexplem  37022  cotrcltrcl  37036  he0  37098  idhe  37101  dvsid  37552  binomcxplemnotnn0  37577  fourierdlem62  39061  fourierdlem66  39065  nbgr2vtx1edg  40572  nbuhgr2vtx1edgb  40574
 Copyright terms: Public domain W3C validator