Theorem subid1d 11492

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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  (class class class)co 7363  ℂcc 11034  0cc0 11036   − cmin 11375

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 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pow 5301  ax-pr 5369  ax-un 7685  ax-resscn 11093  ax-1cn 11094  ax-icn 11095  ax-addcl 11096  ax-addrcl 11097  ax-mulcl 11098  ax-mulrcl 11099  ax-mulcom 11100  ax-addass 11101  ax-mulass 11102  ax-distr 11103  ax-i2m1 11104  ax-1ne0 11105  ax-1rid 11106  ax-rnegex 11107  ax-rrecex 11108  ax-cnre 11109  ax-pre-lttri 11110  ax-pre-lttrn 11111  ax-pre-ltadd 11112

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-nel 3040  df-ral 3055  df-rex 3065  df-reu 3346  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-po 5533  df-so 5534  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7320  df-ov 7366  df-oprab 7367  df-mpo 7368  df-er 8640  df-en 8891  df-dom 8892  df-sdom 8893  df-pnf 11179  df-mnf 11180  df-ltxr 11182  df-sub 11377

This theorem is referenced by:  suble0  11662  lesub0  11665  ltm1  11995  nn0sub  12485  max0sub  13146  modid  13853  modeqmodmin  13901  muldivbinom2  14223  bcn0  14270  bcnn  14272  hashfzo0  14390  hashfz0  14392  ccatlid  14547  pfxmpt  14639  pfxfv  14643  swrdpfx  14667  pfxpfx  14668  cshwsublen  14756  remul2  15090  clim0c  15467  rlimrecl  15540  o1rlimmul  15579  rlimno1  15614  incexclem  15799  supcvg  15819  pwdif  15831  geolim  15833  fallfacval3  15975  binomfallfaclem2  16003  bpolydiflem  16017  bpoly3  16021  addmodlteqALT  16292  dvdsmod  16296  ndvdssub  16376  nn0seqcvgd  16537  phiprmpw  16744  pczpre  16816  pcaddlem  16857  pcmpt2  16862  prmreclem4  16888  4sqlem9  16915  4sqlem11  16924  ramcl  16998  oddvdsnn0  19517  odf1o2  19546  srgbinomlem4  20208  zndvds0  21532  freshmansdream  21556  psrlidm  21943  psdmul  22161  coe1sclmul  22275  coe1sclmul2  22277  cply1mul  22289  recld2  24805  i1fadd  25687  mbfi1fseqlem6  25712  itgposval  25788  dveflem  25971  dv11cn  25993  lhop1lem  26005  coemulc  26245  plydivlem3  26286  plyrem  26296  vieta1lem2  26302  aareccl  26317  aalioulem3  26325  aaliou2b  26332  dvntaylp  26361  taylthlem1  26363  psercn  26416  pserdvlem2  26418  abelthlem2  26422  abelthlem3  26423  abelthlem5  26425  abelthlem7  26428  sinmpi  26476  cosppi  26479  sinhalfpim  26482  sincosq2sgn  26488  logcnlem3  26633  logcnlem4  26634  advlog  26643  efopn  26647  logtayl  26649  pythag  26806  chordthmlem5  26825  atanlogsublem  26904  rlimcnp  26954  efrlim  26958  rlimcxp  26962  cxploglim2  26967  emcllem5  26988  zetacvg  27003  lgamgulmlem2  27018  lgamcvg2  27043  0sgmppw  27186  ppiub  27192  chtublem  27199  logfacrlim  27212  logexprlim  27213  chtppilimlem2  27462  rplogsumlem2  27473  dchrisumlem3  27479  dchrvmasumiflem1  27489  dchrisum0lem2  27506  selberg2lem  27538  logdivbnd  27544  pntrsumo1  27553  pntrlog2bndlem4  27568  pntpbnd1  27574  axlowdimlem17  29052  crctcshlem4  29913  clwlkclwwlklem2a1  30087  clwlkclwwlklem2a  30093  clwlkclwwlklem3  30096  clwlkclwwlk  30097  ipidsq  30806  nmcfnexi  32147  sgnsub  32936  esplyind  33766  vietalem  33770  constrrtcc  33926  nn0constr  33952  constraddcl  33953  constrnegcl  33954  constrdircl  33956  constrremulcl  33958  constrrecl  33960  constrimcl  33961  constrmulcl  33962  constrreinvcl  33963  constrinvcl  33964  constrresqrtcl  33968  constrabscl  33969  cos9thpiminplylem1  33973  cos9thpinconstrlem1  33980  knoppndvlem10  36834  poimirlem19  38013  poimirlem20  38014  ftc1anc  38075  cntotbnd  38170  aks4d1p1p2  42562  aks4d1p1p7  42566  posbezout  42592  bcled  42670  irrapxlem3  43276  irrapxlem4  43277  pell14qrgt0  43311  pell1qrgaplem  43325  acongeq  43435  jm2.18  43440  hashnzfz  44771  hashnzfz2  44772  hashnzfzclim  44773  bccn1  44795  binomcxplemnotnn0  44807  dstregt0  45737  absimlere  45929  ellimcabssub0  46069  0ellimcdiv  46099  clim0cf  46104  fprodsubrecnncnvlem  46357  ioodvbdlimc2lem  46384  dvnxpaek  46392  dvnmul  46393  itgsbtaddcnst  46432  stoweidlem7  46457  stoweidlem11  46461  stoweidlem26  46476  dirkertrigeqlem2  46549  fourierdlem57  46613  fourierdlem60  46616  fourierdlem61  46617  fourierdlem68  46624  fourierdlem104  46660  fourierdlem107  46663  fourierdlem109  46665  etransclem4  46688  etransclem23  46707  etransclem27  46711  etransclem31  46715  etransclem35  46719  sigarexp  47309  sigaradd  47316  m1modmmod  47834  dignn0flhalflem1  49113  ehl2eudisval0  49223  2sphere0  49248  line2  49250  line2x  49252  itschlc0yqe  49258  itschlc0xyqsol1  49264  itschlc0xyqsol  49265