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

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

Proof of Theorem negeq
StepHypRef Expression
1 oveq2 6304 . 2
2 df-neg 9831 . 2
3 df-neg 9831 . 2
41, 2, 33eqtr4g 2523 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  (class class class)co 6296  0cc0 9513   cmin 9828  -ucneg 9829
This theorem is referenced by:  negeqi  9836  negeqd  9837  neg11  9893  renegcl  9905  infm3lem  10526  infm3  10527  riotaneg  10543  negiso  10544  infmsup  10546  infmrcl  10547  elz  10891  elz2  10906  znegcl  10924  zindd  10990  zriotaneg  11002  ublbneg  11195  eqreznegel  11196  negn0  11197  supminf  11198  zsupss  11200  qnegcl  11228  xnegeq  11435  ceilval  11967  expneg  12174  m1expcl2  12188  sqeqor  12282  sqrmo  13085  dvdsnegb  14001  pcexp  14383  pcneg  14397  mulgneg2  16169  negfcncf  21423  xrhmeo  21446  evth2  21460  volsup2  22014  mbfi1fseqlem2  22123  mbfi1fseq  22128  lhop2  22416  lognegb  22974  lgsdir2lem4  23601  rpvmasum2  23697  gxval  25260  gxnn0neg  25265  itgaddnclem2  30074  ftc1anclem5  30094  areacirc  30112  rexzrexnn0  30737  dvdsrabdioph  30743  monotoddzzfi  30878  monotoddzz  30879  oddcomabszz  30880  lcmneg  31209  etransclem17  32034  etransclem46  32063  etransclem47  32064  2zrngagrp  32749  renegclALT  34694
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-iota 5556  df-fv 5601  df-ov 6299  df-neg 9831
  Copyright terms: Public domain W3C validator