Theorem subid1d 11529

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  (class class class)co 7390  ℂcc 11073  0cc0 11075   − cmin 11412

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-po 5549  df-so 5550  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-riota 7347  df-ov 7393  df-oprab 7394  df-mpo 7395  df-er 8674  df-en 8922  df-dom 8923  df-sdom 8924  df-pnf 11217  df-mnf 11218  df-ltxr 11220  df-sub 11414

This theorem is referenced by:  suble0  11699  lesub0  11702  ltm1  12031  nn0sub  12499  max0sub  13163  modid  13865  modeqmodmin  13913  muldivbinom2  14235  bcn0  14282  bcnn  14284  hashfzo0  14402  hashfz0  14404  ccatlid  14558  pfxmpt  14650  pfxfv  14654  swrdpfx  14679  pfxpfx  14680  cshwsublen  14768  remul2  15103  clim0c  15480  rlimrecl  15553  o1rlimmul  15592  rlimno1  15627  incexclem  15809  supcvg  15829  pwdif  15841  geolim  15843  fallfacval3  15985  binomfallfaclem2  16013  bpolydiflem  16027  bpoly3  16031  addmodlteqALT  16302  dvdsmod  16306  ndvdssub  16386  nn0seqcvgd  16547  phiprmpw  16753  pczpre  16825  pcaddlem  16866  pcmpt2  16871  prmreclem4  16897  4sqlem9  16924  4sqlem11  16933  ramcl  17007  oddvdsnn0  19481  odf1o2  19510  srgbinomlem4  20145  zndvds0  21467  freshmansdream  21491  psrlidm  21878  psdmul  22060  coe1sclmul  22175  coe1sclmul2  22177  cply1mul  22190  recld2  24710  i1fadd  25603  mbfi1fseqlem6  25628  itgposval  25704  dveflem  25890  dv11cn  25913  lhop1lem  25925  coemulc  26167  plydivlem3  26210  plyrem  26220  vieta1lem2  26226  aareccl  26241  aalioulem3  26249  aaliou2b  26256  dvntaylp  26286  taylthlem1  26288  psercn  26343  pserdvlem2  26345  abelthlem2  26349  abelthlem3  26350  abelthlem5  26352  abelthlem7  26355  sinmpi  26403  cosppi  26406  sinhalfpim  26409  sincosq2sgn  26415  logcnlem3  26560  logcnlem4  26561  advlog  26570  efopn  26574  logtayl  26576  pythag  26734  chordthmlem5  26753  atanlogsublem  26832  rlimcnp  26882  efrlim  26886  efrlimOLD  26887  rlimcxp  26891  cxploglim2  26896  emcllem5  26917  zetacvg  26932  lgamgulmlem2  26947  lgamcvg2  26972  0sgmppw  27116  ppiub  27122  chtublem  27129  logfacrlim  27142  logexprlim  27143  chtppilimlem2  27392  rplogsumlem2  27403  dchrisumlem3  27409  dchrvmasumiflem1  27419  dchrisum0lem2  27436  selberg2lem  27468  logdivbnd  27474  pntrsumo1  27483  pntrlog2bndlem4  27498  pntpbnd1  27504  axlowdimlem17  28892  crctcshlem4  29757  clwlkclwwlklem2a1  29928  clwlkclwwlklem2a  29934  clwlkclwwlklem3  29937  clwlkclwwlk  29938  ipidsq  30646  nmcfnexi  31987  sgnsub  32769  constrrtcc  33732  nn0constr  33758  constraddcl  33759  constrnegcl  33760  constrdircl  33762  constrremulcl  33764  constrrecl  33766  constrimcl  33767  constrmulcl  33768  constrreinvcl  33769  constrinvcl  33770  constrresqrtcl  33774  constrabscl  33775  cos9thpiminplylem1  33779  cos9thpinconstrlem1  33786  knoppndvlem10  36516  poimirlem19  37640  poimirlem20  37641  ftc1anc  37702  cntotbnd  37797  aks4d1p1p2  42065  aks4d1p1p7  42069  posbezout  42095  bcled  42173  irrapxlem3  42819  irrapxlem4  42820  pell14qrgt0  42854  pell1qrgaplem  42868  acongeq  42979  jm2.18  42984  hashnzfz  44316  hashnzfz2  44317  hashnzfzclim  44318  bccn1  44340  binomcxplemnotnn0  44352  dstregt0  45287  absimlere  45482  ellimcabssub0  45622  0ellimcdiv  45654  clim0cf  45659  fprodsubrecnncnvlem  45912  ioodvbdlimc2lem  45939  dvnxpaek  45947  dvnmul  45948  itgsbtaddcnst  45987  stoweidlem7  46012  stoweidlem11  46016  stoweidlem26  46031  dirkertrigeqlem2  46104  fourierdlem57  46168  fourierdlem60  46171  fourierdlem61  46172  fourierdlem68  46179  fourierdlem104  46215  fourierdlem107  46218  fourierdlem109  46220  etransclem4  46243  etransclem23  46262  etransclem27  46266  etransclem31  46270  etransclem35  46274  sigarexp  46864  sigaradd  46871  m1modmmod  47363  dignn0flhalflem1  48608  ehl2eudisval0  48718  2sphere0  48743  line2  48745  line2x  48747  itschlc0yqe  48753  itschlc0xyqsol1  48759  itschlc0xyqsol  48760