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

Theorem eqimssi 3553
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 3518 . 2  |-  A  C_  A
2 eqimssi.1 . 2  |-  A  =  B
31, 2sseqtri 3531 1  |-  A  C_  B
Colors of variables: wff setvar class
Syntax hints:    = wceq 1395    C_ wss 3471
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-in 3478  df-ss 3485
This theorem is referenced by:  funi  5624  fpr  6080  tz7.48-2  7125  trcl  8176  zorn2lem4  8896  zmin  11203  elfzo1  11870  om2uzf1oi  12067  sumsplit  13595  isumless  13669  frlmip  18936  ust0  20848  rrxprds  21947  rrxip  21948  ovoliunnul  22044  vitalilem5  22147  logtayl  23167  mayetes3i  26775  eulerpartlemsv2  28494  eulerpartlemsv3  28497  eulerpartlemv  28500  eulerpartlemb  28504  dvasin  30308  dvsid  31440  binomcxplemnotnn0  31465  fourierdlem62  32154  fourierdlem66  32158  0trrel  37936  he0  37997  idhe  38000
  Copyright terms: Public domain W3C validator