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

Theorem eqimss2i 4023
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 3986 . 2 𝐵𝐵
2 eqimssi.1 . 2 𝐴 = 𝐵
31, 2sseqtrri 4001 1 𝐵𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1528  wss 3933
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-in 3940  df-ss 3949
This theorem is referenced by:  cotr3  14326  supcvg  15199  prodfclim1  15237  ef0lem  15420  1strbas  16587  restid  16695  cayley  18471  gsumval3  18956  gsumzaddlem  18970  kgencn3  22094  hmeores  22307  opnfbas  22378  tsmsf1o  22680  ust0  22755  icchmeo  23472  plyeq0lem  24727  ulmdvlem1  24915  basellem7  25591  basellem9  25593  dchrisumlem3  25994  structvtxvallem  26732  struct2griedg  26740  cycpmfvlem  30681  cycpmfv3  30684  ivthALT  33580  aomclem4  39535  hashnzfzclim  40531  binomcxplemrat  40559  climsuselem1  41764  gsumfsupp  43966
  Copyright terms: Public domain W3C validator