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

Theorem eqimss2i 3644
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 3608 . 2 𝐵𝐵
2 eqimssi.1 . 2 𝐴 = 𝐵
31, 2sseqtr4i 3622 1 𝐵𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1480  wss 3559
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-in 3566  df-ss 3573
This theorem is referenced by:  cotr3  13659  supcvg  14524  prodfclim1  14561  ef0lem  14745  1strbas  15912  restid  16026  cayley  17766  gsumval3  18240  gsumzaddlem  18253  kgencn3  21284  hmeores  21497  opnfbas  21569  tsmsf1o  21871  ust0  21946  icchmeo  22663  plyeq0lem  23887  ulmdvlem1  24075  basellem7  24730  basellem9  24732  dchrisumlem3  25097  structvtxvallem  25826  struct2griedg  25837  ivthALT  32007  aomclem4  37142  hashnzfzclim  38038  binomcxplemrat  38066  climsuselem1  39271
  Copyright terms: Public domain W3C validator