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

Theorem eqimssi 3946
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 3910 . 2 𝐴𝐴
2 eqimssi.1 . 2 𝐴 = 𝐵
31, 2sseqtri 3924 1 𝐴𝐵
Colors of variables: wff setvar class
Syntax hints:   = wceq 1522  wss 3859
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-in 3866  df-ss 3874
This theorem is referenced by:  funi  6257  fpr  6779  tz7.48-2  7929  trcl  9016  zorn2lem4  9767  zmin  12193  elfzo1  12937  om2uzf1oi  13171  0trrel  14175  sumsplit  14956  isumless  15033  frlmip  20604  ust0  22511  rrxprds  23675  rrxip  23676  ovoliunnul  23791  vitalilem5  23896  logtayl  24924  nbgr2vtx1edg  26815  nbuhgr2vtx1edgb  26817  mayetes3i  29197  cycpmconjslem2  30435  eulerpartlemsv2  31233  eulerpartlemsv3  31236  eulerpartlemv  31239  eulerpartlemb  31243  poimirlem9  34432  dvasin  34509  dmcoss3  35224  disjALTVid  35516  cnvrcl0  39470  corclrcl  39537  trclrelexplem  39541  cotrcltrcl  39555  he0  39615  dvsid  40201  binomcxplemnotnn0  40226  fourierdlem62  41995  fourierdlem66  41999
  Copyright terms: Public domain W3C validator