Theorem subid1d 11583

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  (class class class)co 7405  ℂcc 11127  0cc0 11129   − cmin 11466

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7729  ax-resscn 11186  ax-1cn 11187  ax-icn 11188  ax-addcl 11189  ax-addrcl 11190  ax-mulcl 11191  ax-mulrcl 11192  ax-mulcom 11193  ax-addass 11194  ax-mulass 11195  ax-distr 11196  ax-i2m1 11197  ax-1ne0 11198  ax-1rid 11199  ax-rnegex 11200  ax-rrecex 11201  ax-cnre 11202  ax-pre-lttri 11203  ax-pre-lttrn 11204  ax-pre-ltadd 11205

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 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-po 5561  df-so 5562  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6484  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-riota 7362  df-ov 7408  df-oprab 7409  df-mpo 7410  df-er 8719  df-en 8960  df-dom 8961  df-sdom 8962  df-pnf 11271  df-mnf 11272  df-ltxr 11274  df-sub 11468

This theorem is referenced by:  suble0  11751  lesub0  11754  ltm1  12083  nn0sub  12551  max0sub  13212  modid  13913  modeqmodmin  13959  muldivbinom2  14281  bcn0  14328  bcnn  14330  hashfzo0  14448  hashfz0  14450  ccatlid  14604  pfxmpt  14696  pfxfv  14700  swrdpfx  14725  pfxpfx  14726  cshwsublen  14814  remul2  15149  clim0c  15523  rlimrecl  15596  o1rlimmul  15635  rlimno1  15670  incexclem  15852  supcvg  15872  pwdif  15884  geolim  15886  fallfacval3  16028  binomfallfaclem2  16056  bpolydiflem  16070  bpoly3  16074  addmodlteqALT  16344  dvdsmod  16348  ndvdssub  16428  nn0seqcvgd  16589  phiprmpw  16795  pczpre  16867  pcaddlem  16908  pcmpt2  16913  prmreclem4  16939  4sqlem9  16966  4sqlem11  16975  ramcl  17049  oddvdsnn0  19525  odf1o2  19554  srgbinomlem4  20189  zndvds0  21511  freshmansdream  21535  psrlidm  21922  psdmul  22104  coe1sclmul  22219  coe1sclmul2  22221  cply1mul  22234  recld2  24754  i1fadd  25648  mbfi1fseqlem6  25673  itgposval  25749  dveflem  25935  dv11cn  25958  lhop1lem  25970  coemulc  26212  plydivlem3  26255  plyrem  26265  vieta1lem2  26271  aareccl  26286  aalioulem3  26294  aaliou2b  26301  dvntaylp  26331  taylthlem1  26333  psercn  26388  pserdvlem2  26390  abelthlem2  26394  abelthlem3  26395  abelthlem5  26397  abelthlem7  26400  sinmpi  26448  cosppi  26451  sinhalfpim  26454  sincosq2sgn  26460  logcnlem3  26605  logcnlem4  26606  advlog  26615  efopn  26619  logtayl  26621  pythag  26779  chordthmlem5  26798  atanlogsublem  26877  rlimcnp  26927  efrlim  26931  efrlimOLD  26932  rlimcxp  26936  cxploglim2  26941  emcllem5  26962  zetacvg  26977  lgamgulmlem2  26992  lgamcvg2  27017  0sgmppw  27161  ppiub  27167  chtublem  27174  logfacrlim  27187  logexprlim  27188  chtppilimlem2  27437  rplogsumlem2  27448  dchrisumlem3  27454  dchrvmasumiflem1  27464  dchrisum0lem2  27481  selberg2lem  27513  logdivbnd  27519  pntrsumo1  27528  pntrlog2bndlem4  27543  pntpbnd1  27549  axlowdimlem17  28937  crctcshlem4  29802  clwlkclwwlklem2a1  29973  clwlkclwwlklem2a  29979  clwlkclwwlklem3  29982  clwlkclwwlk  29983  ipidsq  30691  nmcfnexi  32032  sgnsub  32816  constrrtcc  33769  nn0constr  33795  constraddcl  33796  constrnegcl  33797  constrdircl  33799  constrremulcl  33801  constrrecl  33803  constrimcl  33804  constrmulcl  33805  constrreinvcl  33806  constrinvcl  33807  constrresqrtcl  33811  constrabscl  33812  cos9thpiminplylem1  33816  cos9thpinconstrlem1  33823  knoppndvlem10  36539  poimirlem19  37663  poimirlem20  37664  ftc1anc  37725  cntotbnd  37820  aks4d1p1p2  42083  aks4d1p1p7  42087  posbezout  42113  bcled  42191  irrapxlem3  42847  irrapxlem4  42848  pell14qrgt0  42882  pell1qrgaplem  42896  acongeq  43007  jm2.18  43012  hashnzfz  44344  hashnzfz2  44345  hashnzfzclim  44346  bccn1  44368  binomcxplemnotnn0  44380  dstregt0  45310  absimlere  45506  ellimcabssub0  45646  0ellimcdiv  45678  clim0cf  45683  fprodsubrecnncnvlem  45936  ioodvbdlimc2lem  45963  dvnxpaek  45971  dvnmul  45972  itgsbtaddcnst  46011  stoweidlem7  46036  stoweidlem11  46040  stoweidlem26  46055  dirkertrigeqlem2  46128  fourierdlem57  46192  fourierdlem60  46195  fourierdlem61  46196  fourierdlem68  46203  fourierdlem104  46239  fourierdlem107  46242  fourierdlem109  46244  etransclem4  46267  etransclem23  46286  etransclem27  46290  etransclem31  46294  etransclem35  46298  sigarexp  46888  sigaradd  46895  m1modmmod  48501  dignn0flhalflem1  48595  ehl2eudisval0  48705  2sphere0  48730  line2  48732  line2x  48734  itschlc0yqe  48740  itschlc0xyqsol1  48746  itschlc0xyqsol  48747