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

Theorem eqimss2i 3544
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 3508 . 2  |-  B  C_  B
2 eqimssi.1 . 2  |-  A  =  B
31, 2sseqtr4i 3522 1  |-  B  C_  A
Colors of variables: wff setvar class
Syntax hints:    = wceq 1398    C_ wss 3461
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-in 3468  df-ss 3475
This theorem is referenced by:  cotr3  12896  supcvg  13749  prodfclim1  13784  ef0lem  13896  1strbas  14821  restid  14923  cayley  16638  gsumval3OLD  17107  gsumval3  17110  gsumzaddlem  17133  gsumzaddlemOLD  17135  kgencn3  20225  hmeores  20438  opnfbas  20509  tsmsf1o  20813  ust0  20888  icchmeo  21607  plyeq0lem  22773  ulmdvlem1  22961  basellem7  23558  basellem9  23560  dchrisumlem3  23874  ivthALT  30393  aomclem4  31242  hashnzfzclim  31468  binomcxplemrat  31496  climsuselem1  31852
  Copyright terms: Public domain W3C validator