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

Theorem eqimss2i 4045
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 4006 . 2 𝐵𝐵
2 eqimssi.1 . 2 𝐴 = 𝐵
31, 2sseqtrri 4033 1 𝐵𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1540  wss 3951
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-ss 3968
This theorem is referenced by:  cotr3  15017  supcvg  15892  prodfclim1  15929  ef0lem  16114  1strbas  17263  1strbasOLD  17264  restid  17478  cayley  19432  gsumval3  19925  gsumzaddlem  19939  kgencn3  23566  hmeores  23779  opnfbas  23850  tsmsf1o  24153  ust0  24228  icchmeo  24971  icchmeoOLD  24972  plyeq0lem  26249  ulmdvlem1  26443  basellem7  27130  basellem9  27132  dchrisumlem3  27535  structvtxvallem  29037  struct2griedg  29045  gsumhashmul  33064  cycpmfvlem  33132  cycpmfv3  33135  constr01  33783  ivthALT  36336  aomclem4  43069  hashnzfzclim  44341  binomcxplemrat  44369  climsuselem1  45622  gsumfsupp  48098
  Copyright terms: Public domain W3C validator