Theorem subid1d 11661

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 11581	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 − 0) = 𝐴)
3	1, 2	syl 18	1 ⊢ (𝜑 → (𝐴 − 0) = 𝐴)

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  (class class class)co 7420  ℂcc 11201  0cc0 11203   − cmin 11544

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-resscn 11260  ax-1cn 11261  ax-icn 11262  ax-addcl 11263  ax-addrcl 11264  ax-mulcl 11265  ax-mulrcl 11266  ax-mulcom 11267  ax-addass 11268  ax-mulass 11269  ax-distr 11270  ax-i2m1 11271  ax-1ne0 11272  ax-1rid 11273  ax-rnegex 11274  ax-rrecex 11275  ax-cnre 11276  ax-pre-lttri 11277  ax-pre-lttrn 11278  ax-pre-ltadd 11279

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-po 5558  df-so 5559  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7377  df-ov 7423  df-oprab 7424  df-mpo 7425  df-er 8720  df-en 8977  df-dom 8978  df-sdom 8979  df-pnf 11348  df-mnf 11349  df-ltxr 11351  df-sub 11546

This theorem is used by:  suble0  11833  lesub0  11836  ltm1  12162  nn0sub  12659  max0sub  13329  modid  14039  modeqmodmin  14087  muldivbinom2  14410  bcn0  14457  bcnn  14459  hashfzo0  14578  hashfz0  14580  ccatlid  14735  pfxmpt  14832  pfxfv  14836  swrdpfx  14860  pfxpfx  14861  cshwsublen  14951  sgnsub  15264  remul2  15302  clim0c  15679  rlimrecl  15752  o1rlimmul  15791  rlimno1  15826  incexclem  16010  supcvg  16030  pwdif  16042  geolim  16044  fallfacval3  16184  binomfallfaclem2  16211  bpolydiflem  16225  bpoly3  16229  addmodlteqALT  16500  dvdsmod  16504  ndvdssub  16584  nn0seqcvgd  16750  phiprmpw  16958  pczpre  17030  pcaddlem  17071  pcmpt2  17076  prmreclem4  17102  4sqlem9  17129  4sqlem11  17138  ramcl  17212  oddvdsnn0  19763  odf1o2  19792  srgbinomlem4  20460  zndvds0  21861  freshmansdream  21885  psrlidm  22274  psdmul  22492  coe1sclmul  22606  coe1sclmul2  22608  cply1mul  22619  recld2  25139  i1fadd  26021  mbfi1fseqlem6  26046  itgposval  26121  dveflem  26304  dv11cn  26326  lhop1lem  26338  coemulc  26579  plydivlem3  26621  plyrem  26631  vieta1lem2  26639  aareccl  26658  aalioulem3  26666  aaliou2b  26673  dvntaylp  26703  taylthlem1  26705  psercn  26758  pserdvlem2  26760  abelthlem2  26764  abelthlem3  26765  abelthlem5  26767  abelthlem7  26770  sinmpi  26821  cosppi  26824  sinhalfpim  26827  sincosq2sgn  26833  logcnlem3  26977  logcnlem4  26978  advlog  26987  efopn  26991  logtayl  26993  pythag  27150  chordthmlem5  27169  atanlogsublem  27248  rlimcnp  27298  efrlim  27302  rlimcxp  27306  cxploglim2  27311  emcllem5  27332  zetacvg  27347  lgamgulmlem2  27362  lgamcvg2  27387  0sgmppw  27530  ppiub  27536  chtublem  27543  logfacrlim  27556  logexprlim  27557  chtppilimlem2  27806  rplogsumlem2  27817  dchrisumlem3  27823  dchrvmasumiflem1  27833  dchrisum0lem2  27850  selberg2lem  27882  logdivbnd  27888  pntrsumo1  27897  pntrlog2bndlem4  27912  pntpbnd1  27918  axlowdimlem17  29541  crctcshlem4  30414  clwlkclwwlklem2a1  30588  clwlkclwwlklem2a  30594  clwlkclwwlklem3  30597  clwlkclwwlk  30598  ipidsq  31317  nmcfnexi  32658  esplyind  34253  vietalem  34257  constrrtcc  34413  nn0constr  34439  constraddcl  34440  constrnegcl  34441  constrdircl  34443  constrremulcl  34445  constrrecl  34447  constrimcl  34448  constrmulcl  34449  constrreinvcl  34450  constrinvcl  34451  constrresqrtcl  34455  constrabscl  34456  cos9thpiminplylem1  34460  cos9thpinconstrlem1  34467  knoppndvlem10  37479  poimirlem19  38650  poimirlem20  38651  ftc1anc  38712  cntotbnd  38823  aks4d1p1p2  43213  aks4d1p1p7  43217  posbezout  43243  bcled  43321  irrapxlem3  43924  irrapxlem4  43925  pell14qrgt0  43959  pell1qrgaplem  43973  acongeq  44083  jm2.18  44088  hashnzfz  45397  hashnzfz2  45398  hashnzfzclim  45399  bccn1  45421  binomcxplemnotnn0  45433  dstregt0  46391  absimlere  46582  ellimcabssub0  46722  0ellimcdiv  46752  clim0cf  46757  fprodsubrecnncnvlem  47010  ioodvbdlimc2lem  47037  dvnxpaek  47045  dvnmul  47046  itgsbtaddcnst  47085  stoweidlem7  47110  stoweidlem11  47114  stoweidlem26  47129  dirkertrigeqlem2  47202  fourierdlem57  47266  fourierdlem60  47269  fourierdlem61  47270  fourierdlem68  47277  fourierdlem104  47313  fourierdlem107  47316  fourierdlem109  47318  etransclem4  47341  etransclem23  47360  etransclem27  47364  etransclem31  47368  etransclem35  47372  sigarexp  47962  sigaradd  47969  m1modmmod  48527  dignn0flhalflem1  49820  ehl2eudisval0  49931  2sphere0  49955  line2  49957  line2x  49959  itschlc0yqe  49965  itschlc0xyqsol1  49971  itschlc0xyqsol  49972