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

Theorem eqimss2i 3693
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 3657 . 2 𝐵𝐵
2 eqimssi.1 . 2 𝐴 = 𝐵
31, 2sseqtr4i 3671 1 𝐵𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1523  wss 3607
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-in 3614  df-ss 3621
This theorem is referenced by:  cotr3  13763  supcvg  14632  prodfclim1  14669  ef0lem  14853  1strbas  16027  restid  16141  cayley  17880  gsumval3  18354  gsumzaddlem  18367  kgencn3  21409  hmeores  21622  opnfbas  21693  tsmsf1o  21995  ust0  22070  icchmeo  22787  plyeq0lem  24011  ulmdvlem1  24199  basellem7  24858  basellem9  24860  dchrisumlem3  25225  structvtxvallem  25954  struct2griedg  25965  ivthALT  32455  aomclem4  37944  hashnzfzclim  38838  binomcxplemrat  38866  climsuselem1  40157
  Copyright terms: Public domain W3C validator