Theorem subid1d 11332

Description: Identity law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
negidd.1	⊢ (𝜑 → 𝐴 ∈ ℂ)

Assertion

Ref	Expression
subid1d	⊢ (𝜑 → (𝐴 − 0) = 𝐴)

Proof of Theorem subid1d

Step	Hyp	Ref	Expression
1		negidd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		subid1 11252	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 − 0) = 𝐴)
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴 − 0) = 𝐴)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2110  (class class class)co 7272  ℂcc 10880  0cc0 10882   − cmin 11216

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-sep 5227  ax-nul 5234  ax-pow 5292  ax-pr 5356  ax-un 7583  ax-resscn 10939  ax-1cn 10940  ax-icn 10941  ax-addcl 10942  ax-addrcl 10943  ax-mulcl 10944  ax-mulrcl 10945  ax-mulcom 10946  ax-addass 10947  ax-mulass 10948  ax-distr 10949  ax-i2m1 10950  ax-1ne0 10951  ax-1rid 10952  ax-rnegex 10953  ax-rrecex 10954  ax-cnre 10955  ax-pre-lttri 10956  ax-pre-lttrn 10957  ax-pre-ltadd 10958

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-mo 2542  df-eu 2571  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ne 2946  df-nel 3052  df-ral 3071  df-rex 3072  df-reu 3073  df-rab 3075  df-v 3433  df-sbc 3721  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5163  df-id 5490  df-po 5504  df-so 5505  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-iota 6390  df-fun 6434  df-fn 6435  df-f 6436  df-f1 6437  df-fo 6438  df-f1o 6439  df-fv 6440  df-riota 7229  df-ov 7275  df-oprab 7276  df-mpo 7277  df-er 8490  df-en 8726  df-dom 8727  df-sdom 8728  df-pnf 11022  df-mnf 11023  df-ltxr 11025  df-sub 11218

This theorem is referenced by:  suble0  11500  lesub0  11503  ltm1  11828  nn0sub  12294  max0sub  12941  modid  13627  modeqmodmin  13672  muldivbinom2  13988  bcn0  14035  bcnn  14037  hashfzo0  14156  hashfz0  14158  ccatlid  14302  pfxmpt  14402  pfxfv  14406  swrdpfx  14431  pfxpfx  14432  cshwsublen  14520  remul2  14852  clim0c  15227  rlimrecl  15300  o1rlimmul  15339  rlimno1  15376  incexclem  15559  supcvg  15579  pwdif  15591  geolim  15593  fallfacval3  15733  binomfallfaclem2  15761  bpolydiflem  15775  bpoly3  15779  addmodlteqALT  16045  dvdsmod  16049  ndvdssub  16129  nn0seqcvgd  16286  phiprmpw  16488  pczpre  16559  pcaddlem  16600  pcmpt2  16605  prmreclem4  16631  4sqlem9  16658  4sqlem11  16667  ramcl  16741  oddvdsnn0  19163  odf1o2  19189  srgbinomlem4  19790  zndvds0  20769  psrlidm  21183  coe1sclmul  21464  coe1sclmul2  21466  cply1mul  21476  recld2  23988  i1fadd  24870  mbfi1fseqlem6  24896  itgposval  24971  dveflem  25154  dv11cn  25176  lhop1lem  25188  coemulc  25427  plydivlem3  25466  plyrem  25476  vieta1lem2  25482  aareccl  25497  aalioulem3  25505  aaliou2b  25512  dvntaylp  25541  taylthlem1  25543  psercn  25596  pserdvlem2  25598  abelthlem2  25602  abelthlem3  25603  abelthlem5  25605  abelthlem7  25608  sinmpi  25655  cosppi  25658  sinhalfpim  25661  sincosq2sgn  25667  logcnlem3  25810  logcnlem4  25811  advlog  25820  efopn  25824  logtayl  25826  pythag  25978  chordthmlem5  25997  atanlogsublem  26076  rlimcnp  26126  efrlim  26130  rlimcxp  26134  cxploglim2  26139  emcllem5  26160  zetacvg  26175  lgamgulmlem2  26190  lgamcvg2  26215  0sgmppw  26357  ppiub  26363  chtublem  26370  logfacrlim  26383  logexprlim  26384  chtppilimlem2  26633  rplogsumlem2  26644  dchrisumlem3  26650  dchrvmasumiflem1  26660  dchrisum0lem2  26677  selberg2lem  26709  logdivbnd  26715  pntrsumo1  26724  pntrlog2bndlem4  26739  pntpbnd1  26745  axlowdimlem17  27337  crctcshlem4  28194  clwlkclwwlklem2a1  28365  clwlkclwwlklem2a  28371  clwlkclwwlklem3  28374  clwlkclwwlk  28375  ipidsq  29081  nmcfnexi  30422  freshmansdream  31493  sgnsub  32520  knoppndvlem10  34710  poimirlem19  35805  poimirlem20  35806  ftc1anc  35867  cntotbnd  35963  aks4d1p1p2  40087  aks4d1p1p7  40091  irrapxlem3  40655  irrapxlem4  40656  pell14qrgt0  40690  pell1qrgaplem  40704  acongeq  40814  jm2.18  40819  hashnzfz  41920  hashnzfz2  41921  hashnzfzclim  41922  bccn1  41944  binomcxplemnotnn0  41956  dstregt0  42802  absimlere  43002  ellimcabssub0  43140  0ellimcdiv  43172  clim0cf  43177  fprodsubrecnncnvlem  43430  ioodvbdlimc2lem  43457  dvnxpaek  43465  dvnmul  43466  itgsbtaddcnst  43505  stoweidlem7  43530  stoweidlem11  43534  stoweidlem26  43549  dirkertrigeqlem2  43622  fourierdlem57  43686  fourierdlem60  43689  fourierdlem61  43690  fourierdlem68  43697  fourierdlem104  43733  fourierdlem107  43736  fourierdlem109  43738  etransclem4  43761  etransclem23  43780  etransclem27  43784  etransclem31  43788  etransclem35  43792  sigarexp  44354  sigaradd  44361  m1modmmod  45846  dignn0flhalflem1  45940  ehl2eudisval0  46050  2sphere0  46075  line2  46077  line2x  46079  itschlc0yqe  46085  itschlc0xyqsol1  46091  itschlc0xyqsol  46092