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

Theorem eqimss2i 3395
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 3359 . 2  |-  B  C_  B
2 eqimssi.1 . 2  |-  A  =  B
31, 2sseqtr4i 3373 1  |-  B  C_  A
Colors of variables: wff set class
Syntax hints:    = wceq 1652    C_ wss 3312
This theorem is referenced by:  supcvg  12627  ef0lem  12673  restid  13653  cayley  15104  gsumval3  15506  gsumzaddlem  15518  kgencn3  17582  hmeores  17795  opnfbas  17866  tsmsf1o  18166  ust0  18241  icchmeo  18958  plyeq0lem  20121  ulmdvlem1  20308  basellem7  20861  basellem9  20863  dchrisumlem3  21177  prodfclim1  25213  ivthALT  26329  aomclem4  27123  climsuselem1  27700
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-in 3319  df-ss 3326
  Copyright terms: Public domain W3C validator