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

Theorem subid1d 9833
Description: Identity law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
negidd.1  |-  ( ph  ->  A  e.  CC )
Assertion
Ref Expression
subid1d  |-  ( ph  ->  ( A  -  0 )  =  A )

Proof of Theorem subid1d
StepHypRef Expression
1 negidd.1 . 2  |-  ( ph  ->  A  e.  CC )
2 subid1 9752 . 2  |-  ( A  e.  CC  ->  ( A  -  0 )  =  A )
31, 2syl 16 1  |-  ( ph  ->  ( A  -  0 )  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1399    e. wcel 1826  (class class class)co 6196   CCcc 9401   0cc0 9403    - cmin 9718
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-8 1828  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-sep 4488  ax-nul 4496  ax-pow 4543  ax-pr 4601  ax-un 6491  ax-resscn 9460  ax-1cn 9461  ax-icn 9462  ax-addcl 9463  ax-addrcl 9464  ax-mulcl 9465  ax-mulrcl 9466  ax-mulcom 9467  ax-addass 9468  ax-mulass 9469  ax-distr 9470  ax-i2m1 9471  ax-1ne0 9472  ax-1rid 9473  ax-rnegex 9474  ax-rrecex 9475  ax-cnre 9476  ax-pre-lttri 9477  ax-pre-lttrn 9478  ax-pre-ltadd 9479
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-eu 2222  df-mo 2223  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-nel 2580  df-ral 2737  df-rex 2738  df-reu 2739  df-rab 2741  df-v 3036  df-sbc 3253  df-csb 3349  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-nul 3712  df-if 3858  df-pw 3929  df-sn 3945  df-pr 3947  df-op 3951  df-uni 4164  df-br 4368  df-opab 4426  df-mpt 4427  df-id 4709  df-po 4714  df-so 4715  df-xp 4919  df-rel 4920  df-cnv 4921  df-co 4922  df-dm 4923  df-rn 4924  df-res 4925  df-ima 4926  df-iota 5460  df-fun 5498  df-fn 5499  df-f 5500  df-f1 5501  df-fo 5502  df-f1o 5503  df-fv 5504  df-riota 6158  df-ov 6199  df-oprab 6200  df-mpt2 6201  df-er 7229  df-en 7436  df-dom 7437  df-sdom 7438  df-pnf 9541  df-mnf 9542  df-ltxr 9544  df-sub 9720
This theorem is referenced by:  suble0  9984  lesub0  9987  ltm1  10299  nn0sub  10763  max0sub  11316  modid  11921  modeqmodmin  11959  bcn0  12290  bcnn  12292  hashfzo0  12392  hashfz0  12394  ccatlid  12512  swrd0val  12557  swrd0f  12563  swrdid  12564  swrdswrd0  12598  spllen  12641  splfv1  12642  splfv2a  12643  cshwsublen  12678  cshwlen  12681  repswcshw  12691  remul2  12965  clim0c  13332  rlimrecl  13405  o1rlimmul  13443  rlimno1  13478  incexclem  13650  supcvg  13669  geolim  13681  dvdsmod  14045  ndvdssub  14067  nn0seqcvgd  14201  phiprmpw  14308  pczpre  14373  pcaddlem  14409  pcmpt2  14414  prmreclem4  14439  4sqlem9  14466  4sqlem11  14475  ramcl  14549  oddvdsnn0  16685  odf1o2  16710  srgbinomlem4  17307  psrlidm  18169  psrlidmOLD  18170  coe1sclmul  18436  coe1sclmul2  18438  cply1mul  18448  zndvds0  18680  recld2  21404  i1fadd  22187  mbfi1fseqlem6  22212  itgposval  22287  dveflem  22465  dv11cn  22487  lhop1lem  22499  coemulc  22737  plydivlem3  22776  plyrem  22786  vieta1lem2  22792  aareccl  22807  aalioulem3  22815  aaliou2b  22822  dvntaylp  22851  taylthlem1  22853  psercn  22906  pserdvlem2  22908  abelthlem2  22912  abelthlem3  22913  abelthlem5  22915  abelthlem7  22918  sinmpi  22965  cosppi  22968  sinhalfpim  22971  sincosq2sgn  22977  logcnlem3  23112  logcnlem4  23113  advlog  23122  efopn  23126  logtayl  23128  pythag  23267  chordthmlem5  23283  atanlogsublem  23362  rlimcnp  23412  efrlim  23416  rlimcxp  23420  cxploglim2  23425  emcllem5  23446  0sgmppw  23590  ppiub  23596  chtublem  23603  logfacrlim  23616  logexprlim  23617  chtppilimlem2  23776  rplogsumlem2  23787  dchrisumlem3  23793  dchrvmasumiflem1  23803  dchrisum0lem2  23820  selberg2lem  23852  logdivbnd  23858  pntrsumo1  23867  pntrlog2bndlem4  23882  pntpbnd1  23888  axlowdimlem17  24382  clwlkisclwwlklem2a1  24900  clwlkisclwwlklem2a  24906  clwlkisclwwlklem0  24909  clwlkisclwwlk  24910  ipidsq  25740  nmcfnexi  27086  sgnsub  28666  zetacvg  28746  lgamgulmlem2  28761  lgamcvg2  28786  fallfacval3  29300  binomfallfaclem2  29328  bpolydiflem  29969  bpoly3  29973  ftc1anc  30264  cntotbnd  30458  irrapxlem3  30925  irrapxlem4  30926  pell14qrgt0  30960  pell1qrgaplem  30974  acongeq  31086  dvdsabsmod0OLD  31094  jm2.18  31096  hashnzfz  31393  hashnzfz2  31394  hashnzfzclim  31395  bccn1  31417  binomcxplemnotnn0  31429  dstregt0  31630  ellimcabssub0  31789  0ellimcdiv  31821  clim0cf  31826  ioodvbdlimc2lem  31897  dvnxpaek  31905  dvnmul  31906  itgsbtaddcnst  31947  stoweidlem7  31955  stoweidlem11  31959  stoweidlem26  31974  dirkertrigeqlem2  32047  fourierdlem57  32112  fourierdlem60  32115  fourierdlem61  32116  fourierdlem68  32123  fourierdlem104  32159  fourierdlem107  32162  fourierdlem109  32164  etransclem4  32187  etransclem23  32206  etransclem27  32210  etransclem31  32214  etransclem35  32218  sigarexp  32242  sigaradd  32249  pfxmpt  32562  pfxfv  32574  pfxpfx  32590  m1modmmod  33334  dignn0flhalflem1  33436
  Copyright terms: Public domain W3C validator