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

Theorem eqimss2i 3558
 Description: Infer subclass relationship from equality. (Contributed by NM, 7-Jan-2007.)
Hypothesis
Ref Expression
eqimssi.1
Assertion
Ref Expression
eqimss2i

Proof of Theorem eqimss2i
StepHypRef Expression
1 ssid 3522 . 2
2 eqimssi.1 . 2
31, 2sseqtr4i 3536 1
 Colors of variables: wff setvar class Syntax hints:  =wceq 1395  C_wss 3475 This theorem is referenced by:  supcvg  13667  prodfclim1  13702  ef0lem  13814  restid  14831  cayley  16439  gsumval3OLD  16908  gsumval3  16911  gsumzaddlem  16934  gsumzaddlemOLD  16936  kgencn3  20059  hmeores  20272  opnfbas  20343  tsmsf1o  20647  ust0  20722  icchmeo  21441  plyeq0lem  22607  ulmdvlem1  22795  basellem7  23360  basellem9  23362  dchrisumlem3  23676  ivthALT  30153  aomclem4  31003  hashnzfzclim  31227  binomcxplemrat  31255  climsuselem1  31613  1strbas  32561  cotr3  37788 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-in 3482  df-ss 3489
 Copyright terms: Public domain W3C validator