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

Theorem eqimssi 4043
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 4005 . 2 𝐴𝐴
2 eqimssi.1 . 2 𝐴 = 𝐵
31, 2sseqtri 4019 1 𝐴𝐵
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  wss 3949
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966
This theorem is referenced by:  funi  6581  fpr  7152  tz7.48-2  8442  trcl  9723  zorn2lem4  10494  zmin  12928  elfzo1  13682  om2uzf1oi  13918  0trrel  14928  sumsplit  15714  isumless  15791  frlmip  21333  ust0  23724  rrxprds  24906  rrxip  24907  ovoliunnul  25024  vitalilem5  25129  logtayl  26168  nbgr2vtx1edg  28607  nbuhgr2vtx1edgb  28609  mayetes3i  30982  cycpmconjslem2  32314  eulerpartlemsv2  33357  eulerpartlemsv3  33360  eulerpartlemv  33363  eulerpartlemb  33367  poimirlem9  36497  dvasin  36572  dmcoss3  37323  disjALTVid  37625  sticksstones17  40979  sticksstones18  40980  nna4b4nsq  41402  cnvrcl0  42376  corclrcl  42458  trclrelexplem  42462  cotrcltrcl  42476  he0  42535  dvsid  43090  binomcxplemnotnn0  43115  fourierdlem62  44884  fourierdlem66  44888  rnglidl1  46753
  Copyright terms: Public domain W3C validator