Theorem subid1d 11251

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2108  (class class class)co 7255  ℂcc 10800  0cc0 10802   − cmin 11135

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-resscn 10859  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-addrcl 10863  ax-mulcl 10864  ax-mulrcl 10865  ax-mulcom 10866  ax-addass 10867  ax-mulass 10868  ax-distr 10869  ax-i2m1 10870  ax-1ne0 10871  ax-1rid 10872  ax-rnegex 10873  ax-rrecex 10874  ax-cnre 10875  ax-pre-lttri 10876  ax-pre-lttrn 10877  ax-pre-ltadd 10878

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-po 5494  df-so 5495  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-riota 7212  df-ov 7258  df-oprab 7259  df-mpo 7260  df-er 8456  df-en 8692  df-dom 8693  df-sdom 8694  df-pnf 10942  df-mnf 10943  df-ltxr 10945  df-sub 11137

This theorem is referenced by:  suble0  11419  lesub0  11422  ltm1  11747  nn0sub  12213  max0sub  12859  modid  13544  modeqmodmin  13589  muldivbinom2  13905  bcn0  13952  bcnn  13954  hashfzo0  14073  hashfz0  14075  ccatlid  14219  pfxmpt  14319  pfxfv  14323  swrdpfx  14348  pfxpfx  14349  cshwsublen  14437  remul2  14769  clim0c  15144  rlimrecl  15217  o1rlimmul  15256  rlimno1  15293  incexclem  15476  supcvg  15496  pwdif  15508  geolim  15510  fallfacval3  15650  binomfallfaclem2  15678  bpolydiflem  15692  bpoly3  15696  addmodlteqALT  15962  dvdsmod  15966  ndvdssub  16046  nn0seqcvgd  16203  phiprmpw  16405  pczpre  16476  pcaddlem  16517  pcmpt2  16522  prmreclem4  16548  4sqlem9  16575  4sqlem11  16584  ramcl  16658  oddvdsnn0  19067  odf1o2  19093  srgbinomlem4  19694  zndvds0  20670  psrlidm  21082  coe1sclmul  21363  coe1sclmul2  21365  cply1mul  21375  recld2  23883  i1fadd  24764  mbfi1fseqlem6  24790  itgposval  24865  dveflem  25048  dv11cn  25070  lhop1lem  25082  coemulc  25321  plydivlem3  25360  plyrem  25370  vieta1lem2  25376  aareccl  25391  aalioulem3  25399  aaliou2b  25406  dvntaylp  25435  taylthlem1  25437  psercn  25490  pserdvlem2  25492  abelthlem2  25496  abelthlem3  25497  abelthlem5  25499  abelthlem7  25502  sinmpi  25549  cosppi  25552  sinhalfpim  25555  sincosq2sgn  25561  logcnlem3  25704  logcnlem4  25705  advlog  25714  efopn  25718  logtayl  25720  pythag  25872  chordthmlem5  25891  atanlogsublem  25970  rlimcnp  26020  efrlim  26024  rlimcxp  26028  cxploglim2  26033  emcllem5  26054  zetacvg  26069  lgamgulmlem2  26084  lgamcvg2  26109  0sgmppw  26251  ppiub  26257  chtublem  26264  logfacrlim  26277  logexprlim  26278  chtppilimlem2  26527  rplogsumlem2  26538  dchrisumlem3  26544  dchrvmasumiflem1  26554  dchrisum0lem2  26571  selberg2lem  26603  logdivbnd  26609  pntrsumo1  26618  pntrlog2bndlem4  26633  pntpbnd1  26639  axlowdimlem17  27229  crctcshlem4  28086  clwlkclwwlklem2a1  28257  clwlkclwwlklem2a  28263  clwlkclwwlklem3  28266  clwlkclwwlk  28267  ipidsq  28973  nmcfnexi  30314  freshmansdream  31386  sgnsub  32411  knoppndvlem10  34628  poimirlem19  35723  poimirlem20  35724  ftc1anc  35785  cntotbnd  35881  aks4d1p1p2  40006  aks4d1p1p7  40010  irrapxlem3  40562  irrapxlem4  40563  pell14qrgt0  40597  pell1qrgaplem  40611  acongeq  40721  jm2.18  40726  hashnzfz  41827  hashnzfz2  41828  hashnzfzclim  41829  bccn1  41851  binomcxplemnotnn0  41863  dstregt0  42709  absimlere  42910  ellimcabssub0  43048  0ellimcdiv  43080  clim0cf  43085  fprodsubrecnncnvlem  43338  ioodvbdlimc2lem  43365  dvnxpaek  43373  dvnmul  43374  itgsbtaddcnst  43413  stoweidlem7  43438  stoweidlem11  43442  stoweidlem26  43457  dirkertrigeqlem2  43530  fourierdlem57  43594  fourierdlem60  43597  fourierdlem61  43598  fourierdlem68  43605  fourierdlem104  43641  fourierdlem107  43644  fourierdlem109  43646  etransclem4  43669  etransclem23  43688  etransclem27  43692  etransclem31  43696  etransclem35  43700  sigarexp  44262  sigaradd  44269  m1modmmod  45755  dignn0flhalflem1  45849  ehl2eudisval0  45959  2sphere0  45984  line2  45986  line2x  45988  itschlc0yqe  45994  itschlc0xyqsol1  46000  itschlc0xyqsol  46001