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

Theorem eqimssi 3410
Description: Infer subclass relationship from equality. (Contributed by NM, 6-Jan-2007.)
Hypothesis
Ref Expression
eqimssi.1  |-  A  =  B
Assertion
Ref Expression
eqimssi  |-  A  C_  B

Proof of Theorem eqimssi
StepHypRef Expression
1 ssid 3375 . 2  |-  A  C_  A
2 eqimssi.1 . 2  |-  A  =  B
31, 2sseqtri 3388 1  |-  A  C_  B
Colors of variables: wff setvar class
Syntax hints:    = wceq 1369    C_ wss 3328
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-in 3335  df-ss 3342
This theorem is referenced by:  funi  5448  fpr  5890  tz7.48-2  6897  trcl  7948  zorn2lem4  8668  zmin  10949  elfzo1  11595  om2uzf1oi  11776  sumsplit  13235  isumless  13308  frlmip  18203  ust0  19794  rrxprds  20893  ovoliunnul  20990  vitalilem5  21092  logtayl  22105  mayetes3i  25133  eulerpartlemsv2  26741  eulerpartlemsv3  26744  eulerpartlemv  26747  eulerpartlemb  26751  dvasin  28480  dvsid  29605
  Copyright terms: Public domain W3C validator