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 4031 1 𝐴𝐵
Colors of variables: wff setvar class
Syntax hints:   = wceq 1539  wss 3950
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2707
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-cleq 2728  df-ss 3967
This theorem is referenced by:  funi  6597  fpr  7173  tz7.48-2  8483  trcl  9769  zorn2lem4  10540  zmin  12987  elfzo1  13753  om2uzf1oi  13995  0trrel  15021  sumsplit  15805  isumless  15882  rnglidl1  21243  frlmip  21799  ust0  24229  rrxprds  25424  rrxip  25425  ovoliunnul  25543  vitalilem5  25648  logtayl  26703  nbgr2vtx1edg  29368  nbuhgr2vtx1edgb  29370  mayetes3i  31749  cycpmconjslem2  33176  eulerpartlemsv2  34361  eulerpartlemsv3  34364  eulerpartlemv  34367  eulerpartlemb  34371  poimirlem9  37637  dvasin  37712  dmcoss3  38455  disjALTVid  38757  sticksstones17  42165  sticksstones18  42166  nna4b4nsq  42675  cnvrcl0  43643  corclrcl  43725  trclrelexplem  43729  cotrcltrcl  43743  he0  43802  dvsid  44355  binomcxplemnotnn0  44380  wfaxreg  45022  fourierdlem62  46188  fourierdlem66  46192  isubgr3stgrlem6  47943
  Copyright terms: Public domain W3C validator