MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  negeq Unicode version

Theorem negeq 9548
Description: Equality theorem for negatives. (Contributed by NM, 10-Feb-1995.)
Assertion
Ref Expression
negeq

Proof of Theorem negeq
StepHypRef Expression
1 oveq2 6069 . 2
2 df-neg 9544 . 2
3 df-neg 9544 . 2
41, 2, 33eqtr4g 2479 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1687  (class class class)co 6061  0cc0 9228   cmin 9541  -ucneg 9542
This theorem is referenced by:  negeqi  9549  negeqd  9550  neg11  9606  renegcl  9618  infm3lem  10234  infm3  10235  riotaneg  10251  negiso  10252  infmsup  10254  infmrcl  10255  elz  10593  elz2  10608  znegcl  10625  zindd  10688  zriotaneg  10699  ublbneg  10884  eqreznegel  10885  negn0  10886  supminf  10887  zsupss  10889  qnegcl  10915  xnegeq  11122  ceilval  11620  expneg  11814  m1expcl2  11828  sqeqor  11921  sqrmo  12682  dvdsnegb  13490  pcexp  13866  pcneg  13880  mulgneg2  15591  negfcncf  20195  xrhmeo  20218  evth2  20232  volsup2  20785  mbfi1fseqlem2  20894  mbfi1fseq  20899  lhop2  21187  lognegb  21779  lgsdir2lem4  22406  rpvmasum2  22502  gxval  23424  gxnn0neg  23429  itgaddnclem2  28122  ftc1anclem5  28142  areacirc  28160  rexzrexnn0  28815  dvdsrabdioph  28821  monotoddzzfi  28956  monotoddzz  28957  oddcomabszz  28958  renegclALT  32051
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1586  ax-4 1597  ax-5 1661  ax-6 1701  ax-7 1721  ax-10 1768  ax-11 1773  ax-12 1785  ax-13 1934  ax-ext 2403
This theorem depends on definitions:  df-bi 179  df-or 363  df-an 364  df-3an 952  df-tru 1355  df-ex 1582  df-nf 1585  df-sb 1694  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2547  df-rex 2700  df-rab 2703  df-v 2953  df-dif 3308  df-un 3310  df-in 3312  df-ss 3319  df-nul 3615  df-if 3769  df-sn 3859  df-pr 3860  df-op 3862  df-uni 4067  df-br 4268  df-iota 5353  df-fv 5398  df-ov 6064  df-neg 9544
  Copyright terms: Public domain W3C validator