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

Theorem eqimssi 3557
 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 3522 . 2
2 eqimssi.1 . 2
31, 2sseqtri 3535 1
 Colors of variables: wff setvar class Syntax hints:  =wceq 1395  C_wss 3475 This theorem is referenced by:  funi  5623  fpr  6079  tz7.48-2  7126  trcl  8180  zorn2lem4  8900  zmin  11207  elfzo1  11871  om2uzf1oi  12064  sumsplit  13583  isumless  13657  frlmip  18809  ust0  20722  rrxprds  21821  rrxip  21822  ovoliunnul  21918  vitalilem5  22021  logtayl  23041  mayetes3i  26648  eulerpartlemsv2  28297  eulerpartlemsv3  28300  eulerpartlemv  28303  eulerpartlemb  28307  dvasin  30103  dvsid  31236  binomcxplemnotnn0  31261  fourierdlem62  31951  fourierdlem66  31955  0trrel  37776  he0  37807  idhe  37810 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-in 3482  df-ss 3489
 Copyright terms: Public domain W3C validator