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

Theorem eqimss2i 4041
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 4002 . 2 𝐵𝐵
2 eqimssi.1 . 2 𝐴 = 𝐵
31, 2sseqtrri 4017 1 𝐵𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1534  wss 3947
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-9 2109  ax-ext 2697
This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-cleq 2718  df-ss 3964
This theorem is referenced by:  cotr3  14983  supcvg  15860  prodfclim1  15897  ef0lem  16080  1strbas  17230  1strbasOLD  17231  restid  17448  cayley  19412  gsumval3  19905  gsumzaddlem  19919  kgencn3  23553  hmeores  23766  opnfbas  23837  tsmsf1o  24140  ust0  24215  icchmeo  24956  icchmeoOLD  24957  plyeq0lem  26237  ulmdvlem1  26429  basellem7  27115  basellem9  27117  dchrisumlem3  27520  structvtxvallem  28956  struct2griedg  28964  gsumhashmul  32925  cycpmfvlem  32990  cycpmfv3  32993  constr01  33600  ivthALT  36047  aomclem4  42718  hashnzfzclim  43996  binomcxplemrat  44024  climsuselem1  45228  gsumfsupp  47559
  Copyright terms: Public domain W3C validator