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

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

Proof of Theorem eqimss2i
StepHypRef Expression
1 ssid 3470 . 2  |-  B  C_  B
2 eqimssi.1 . 2  |-  A  =  B
31, 2sseqtr4i 3484 1  |-  B  C_  A
Colors of variables: wff setvar class
Syntax hints:    = wceq 1370    C_ wss 3423
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-in 3430  df-ss 3437
This theorem is referenced by:  supcvg  13417  ef0lem  13463  restid  14471  cayley  16018  gsumval3OLD  16483  gsumval3  16486  gsumzaddlem  16509  gsumzaddlemOLD  16511  kgencn3  19244  hmeores  19457  opnfbas  19528  tsmsf1o  19832  ust0  19907  icchmeo  20626  plyeq0lem  21791  ulmdvlem1  21978  basellem7  22537  basellem9  22539  dchrisumlem3  22853  prodfclim1  27539  ivthALT  28665  aomclem4  29545  climsuselem1  29915  cpmadumatpolylem3  31334
  Copyright terms: Public domain W3C validator