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

Theorem eqimss2i 4005
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 3968 . 2 𝐵𝐵
2 eqimssi.1 . 2 𝐴 = 𝐵
31, 2sseqtrri 3983 1 𝐵𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1537  wss 3913
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-12 2177  ax-ext 2792
This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-sb 2070  df-clab 2799  df-cleq 2813  df-clel 2891  df-v 3475  df-in 3920  df-ss 3930
This theorem is referenced by:  cotr3  14318  supcvg  15191  prodfclim1  15229  ef0lem  15412  1strbas  16578  restid  16686  cayley  18521  gsumval3  19006  gsumzaddlem  19020  kgencn3  22142  hmeores  22355  opnfbas  22426  tsmsf1o  22729  ust0  22804  icchmeo  23525  plyeq0lem  24786  ulmdvlem1  24974  basellem7  25651  basellem9  25653  dchrisumlem3  26054  structvtxvallem  26792  struct2griedg  26800  cycpmfvlem  30762  cycpmfv3  30765  ivthALT  33691  aomclem4  39794  hashnzfzclim  40809  binomcxplemrat  40837  climsuselem1  42040  gsumfsupp  44234
  Copyright terms: Public domain W3C validator