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

Theorem subidd 9920
Description: Subtraction of a number from itself. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
negidd.1  |-  ( ph  ->  A  e.  CC )
Assertion
Ref Expression
subidd  |-  ( ph  ->  ( A  -  A
)  =  0 )

Proof of Theorem subidd
StepHypRef Expression
1 negidd.1 . 2  |-  ( ph  ->  A  e.  CC )
2 subid 9839 . 2  |-  ( A  e.  CC  ->  ( A  -  A )  =  0 )
31, 2syl 17 1  |-  ( ph  ->  ( A  -  A
)  =  0 )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437    e. wcel 1872  (class class class)co 6244   CCcc 9483   0cc0 9485    - cmin 9806
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403  ax-sep 4484  ax-nul 4493  ax-pow 4540  ax-pr 4598  ax-un 6536  ax-resscn 9542  ax-1cn 9543  ax-icn 9544  ax-addcl 9545  ax-addrcl 9546  ax-mulcl 9547  ax-mulrcl 9548  ax-mulcom 9549  ax-addass 9550  ax-mulass 9551  ax-distr 9552  ax-i2m1 9553  ax-1ne0 9554  ax-1rid 9555  ax-rnegex 9556  ax-rrecex 9557  ax-cnre 9558  ax-pre-lttri 9559  ax-pre-lttrn 9560  ax-pre-ltadd 9561
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2275  df-mo 2276  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-ne 2596  df-nel 2597  df-ral 2714  df-rex 2715  df-reu 2716  df-rab 2718  df-v 3019  df-sbc 3238  df-csb 3334  df-dif 3377  df-un 3379  df-in 3381  df-ss 3388  df-nul 3700  df-if 3850  df-pw 3921  df-sn 3937  df-pr 3939  df-op 3943  df-uni 4158  df-br 4362  df-opab 4421  df-mpt 4422  df-id 4706  df-po 4712  df-so 4713  df-xp 4797  df-rel 4798  df-cnv 4799  df-co 4800  df-dm 4801  df-rn 4802  df-res 4803  df-ima 4804  df-iota 5503  df-fun 5541  df-fn 5542  df-f 5543  df-f1 5544  df-fo 5545  df-f1o 5546  df-fv 5547  df-riota 6206  df-ov 6247  df-oprab 6248  df-mpt2 6249  df-er 7313  df-en 7520  df-dom 7521  df-sdom 7522  df-pnf 9623  df-mnf 9624  df-ltxr 9626  df-sub 9808
This theorem is referenced by:  leaddle0  10075  cru  10547  iccf1o  11722  fzocatel  11923  zmod10  12058  hashfzo  12544  ccats1val2  12701  swrd00  12715  swrdccat3blem  12792  revccat  12812  repswswrd  12828  climconst  13545  rlimconst  13546  telfsumo  13800  fsumparts  13804  incexc  13833  cvgrat  13877  binomfallfaclem2  14031  fallfacfac  14036  bpolysum  14044  divalglem5OLD  14314  divalglem5  14315  nn0seqcvgd  14467  pcmpt2  14776  4sqlem15OLD  14841  4sqlem15  14847  efgtlen  17314  srgbinomlem3  17713  cayhamlem1  19827  vitalilem1  22503  dvcnp2  22811  dvferm1lem  22873  c1lip1  22886  dv11cn  22890  ftc1lem5  22929  ftc2  22933  plyeq0lem  23101  dgrcolem2  23165  plydivlem4  23186  qaa  23216  aalioulem3  23227  aaliou3lem2  23236  tayl0  23254  dvntaylp  23263  taylthlem1  23265  taylthlem2  23266  abelthlem9  23332  isosctrlem1  23684  birthdaylem2  23815  rlimcnp  23828  lgam1  23926  basellem2  23945  basellem5  23948  chpub  24085  dchrsum2  24133  sumdchr2  24135  rplogsumlem2  24260  dchrisumlem1  24264  pntlemf  24380  colinearalglem4  24876  wlkdvspthlem  25274  ipidsq  26286  dip0r  26293  riesz3i  27652  riesz4i  27653  hmopidmpji  27742  pjclem4  27789  pj3si  27797  2sqmod  28355  signsply0  29387  poimir  31880  itg2addnclem3  31902  ftc1cnnc  31923  ftc2nc  31933  areacirc  31944  congid  35734  congabseq  35737  jm2.18  35756  dgrsub2  35907  areaquad  36014  ofsubid  36586  isosctrlem1ALT  37247  supxrgelem  37457  constlimc  37587  ioodvbdlimc1lem1  37686  ioodvbdlimc1lem1OLD  37688  dvnxpaek  37700  dvnmul  37701  stoweidlem13  37756  stoweidlem23  37766  stoweidlem26  37769  stirlinglem5  37823  dirkertrigeqlem2  37844  fourierdlem4  37856  fourierdlem42  37895  fourierdlem42OLD  37896  fourierdlem60  37913  fourierdlem61  37914  fourierdlem74  37927  fourierdlem75  37928  fourierdlem89  37942  fourierdlem90  37943  fourierdlem91  37944  fourierdlem103  37956  fourierdlem104  37957  fourierdlem107  37960  sqwvfoura  37975  etransclem24  38006  etransclem25  38007  hoidmv1lelem1  38260  hoidmv1lelem2  38261  hoidmvlelem1  38264  hoidmvlelem2  38265  m1mod0mod1  38536  ccatpfx  38763  2elfz2melfz  38855  m1modmmod  39917
  Copyright terms: Public domain W3C validator