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

Theorem subid1d 9393
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 9315 . 2  |-  ( A  e.  CC  ->  ( A  -  0 )  =  A )
31, 2syl 16 1  |-  ( ph  ->  ( A  -  0 )  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652    e. wcel 1725  (class class class)co 6074   CCcc 8981   0cc0 8983    - cmin 9284
This theorem is referenced by:  suble0  9535  lesub0  9537  ltm1  9843  nn0sub  10263  max0sub  10775  modid  11263  bcn0  11594  bcnn  11596  hashfzo0  11688  ccatlid  11741  swrd0val  11761  swrdid  11765  spllen  11776  splfv1  11777  splfv2a  11778  remul2  11928  clim0c  12294  rlimrecl  12367  o1rlimmul  12405  rlimno1  12440  incexclem  12609  supcvg  12628  geolim  12640  dvdsmod  12899  ndvdssub  12920  nn0seqcvgd  13054  phiprmpw  13158  pczpre  13214  pcaddlem  13250  pcmpt2  13255  prmreclem4  13280  4sqlem9  13307  4sqlem11  13316  ramcl  13390  oddvdsnn0  15175  odf1o2  15200  psrlidm  16460  coe1sclmul  16667  coe1sclmul2  16669  zndvds0  16824  recld2  18838  i1fadd  19580  mbfi1fseqlem6  19605  itgposval  19680  dveflem  19856  dv11cn  19878  lhop1lem  19890  coemulc  20166  plydivlem3  20205  plyrem  20215  vieta1lem2  20221  aareccl  20236  aalioulem3  20244  aaliou2b  20251  dvntaylp  20280  taylthlem1  20282  psercn  20335  pserdvlem2  20337  abelthlem2  20341  abelthlem3  20342  abelthlem5  20344  abelthlem7  20347  sinmpi  20388  cosppi  20391  sinhalfpim  20394  sincosq2sgn  20400  logcnlem3  20528  logcnlem4  20529  advlog  20538  efopn  20542  logtayl  20544  pythag  20652  chordthmlem5  20670  atanlogsublem  20748  rlimcnp  20797  efrlim  20801  rlimcxp  20805  cxploglim2  20810  emcllem5  20831  0sgmppw  20975  ppiub  20981  chtublem  20988  logfacrlim  21001  logexprlim  21002  chtppilimlem2  21161  rplogsumlem2  21172  dchrisumlem3  21178  dchrvmasumiflem1  21188  dchrisum0lem2  21205  selberg2lem  21237  logdivbnd  21243  pntrsumo1  21252  pntrlog2bndlem4  21267  pntpbnd1  21273  ipidsq  22202  nmcfnexi  23547  zetacvg  24792  lgamgulmlem2  24807  lgamcvg2  24832  fallfacval3  25321  binomfallfaclem2  25349  axlowdimlem17  25890  bpolydiflem  26093  bpoly3  26097  ftc1anc  26279  cntotbnd  26497  irrapxlem3  26879  irrapxlem4  26880  pell14qrgt0  26914  pell1qrgaplem  26928  acongeq  27040  dvdsabsmod0  27049  jm2.18  27051  stoweidlem7  27724  stoweidlem11  27728  stoweidlem26  27743  sigarexp  27817  sigaradd  27824  hashfzdm  28145  swrd0swrdid  28167  swrdswrd0  28168  cshwidx  28209
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417  ax-sep 4323  ax-nul 4331  ax-pow 4370  ax-pr 4396  ax-un 4694  ax-resscn 9040  ax-1cn 9041  ax-icn 9042  ax-addcl 9043  ax-addrcl 9044  ax-mulcl 9045  ax-mulrcl 9046  ax-mulcom 9047  ax-addass 9048  ax-mulass 9049  ax-distr 9050  ax-i2m1 9051  ax-1ne0 9052  ax-1rid 9053  ax-rnegex 9054  ax-rrecex 9055  ax-cnre 9056  ax-pre-lttri 9057  ax-pre-lttrn 9058  ax-pre-ltadd 9059
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2285  df-mo 2286  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ne 2601  df-nel 2602  df-ral 2703  df-rex 2704  df-reu 2705  df-rab 2707  df-v 2951  df-sbc 3155  df-csb 3245  df-dif 3316  df-un 3318  df-in 3320  df-ss 3327  df-nul 3622  df-if 3733  df-pw 3794  df-sn 3813  df-pr 3814  df-op 3816  df-uni 4009  df-br 4206  df-opab 4260  df-mpt 4261  df-id 4491  df-po 4496  df-so 4497  df-xp 4877  df-rel 4878  df-cnv 4879  df-co 4880  df-dm 4881  df-rn 4882  df-res 4883  df-ima 4884  df-iota 5411  df-fun 5449  df-fn 5450  df-f 5451  df-f1 5452  df-fo 5453  df-f1o 5454  df-fv 5455  df-ov 6077  df-oprab 6078  df-mpt2 6079  df-riota 6542  df-er 6898  df-en 7103  df-dom 7104  df-sdom 7105  df-pnf 9115  df-mnf 9116  df-ltxr 9118  df-sub 9286
  Copyright terms: Public domain W3C validator