Theorem subid1d 11592

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

Syntax hints:   → wi 4   = wceq 1533   ∈ wcel 2098  (class class class)co 7419  ℂcc 11138  0cc0 11140   − cmin 11476

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741  ax-resscn 11197  ax-1cn 11198  ax-icn 11199  ax-addcl 11200  ax-addrcl 11201  ax-mulcl 11202  ax-mulrcl 11203  ax-mulcom 11204  ax-addass 11205  ax-mulass 11206  ax-distr 11207  ax-i2m1 11208  ax-1ne0 11209  ax-1rid 11210  ax-rnegex 11211  ax-rrecex 11212  ax-cnre 11213  ax-pre-lttri 11214  ax-pre-lttrn 11215  ax-pre-ltadd 11216

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5576  df-po 5590  df-so 5591  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-riota 7375  df-ov 7422  df-oprab 7423  df-mpo 7424  df-er 8725  df-en 8965  df-dom 8966  df-sdom 8967  df-pnf 11282  df-mnf 11283  df-ltxr 11285  df-sub 11478

This theorem is referenced by:  suble0  11760  lesub0  11763  ltm1  12089  nn0sub  12555  max0sub  13210  modid  13897  modeqmodmin  13942  muldivbinom2  14258  bcn0  14305  bcnn  14307  hashfzo0  14425  hashfz0  14427  ccatlid  14572  pfxmpt  14664  pfxfv  14668  swrdpfx  14693  pfxpfx  14694  cshwsublen  14782  remul2  15113  clim0c  15487  rlimrecl  15560  o1rlimmul  15599  rlimno1  15636  incexclem  15818  supcvg  15838  pwdif  15850  geolim  15852  fallfacval3  15992  binomfallfaclem2  16020  bpolydiflem  16034  bpoly3  16038  addmodlteqALT  16305  dvdsmod  16309  ndvdssub  16389  nn0seqcvgd  16544  phiprmpw  16748  pczpre  16819  pcaddlem  16860  pcmpt2  16865  prmreclem4  16891  4sqlem9  16918  4sqlem11  16927  ramcl  17001  oddvdsnn0  19511  odf1o2  19540  srgbinomlem4  20181  zndvds0  21501  freshmansdream  21525  psrlidm  21924  psdmul  22113  coe1sclmul  22226  coe1sclmul2  22228  cply1mul  22240  recld2  24774  i1fadd  25668  mbfi1fseqlem6  25694  itgposval  25769  dveflem  25955  dv11cn  25978  lhop1lem  25990  coemulc  26234  plydivlem3  26275  plyrem  26285  vieta1lem2  26291  aareccl  26306  aalioulem3  26314  aaliou2b  26321  dvntaylp  26351  taylthlem1  26353  psercn  26408  pserdvlem2  26410  abelthlem2  26414  abelthlem3  26415  abelthlem5  26417  abelthlem7  26420  sinmpi  26467  cosppi  26470  sinhalfpim  26473  sincosq2sgn  26479  logcnlem3  26623  logcnlem4  26624  advlog  26633  efopn  26637  logtayl  26639  pythag  26794  chordthmlem5  26813  atanlogsublem  26892  rlimcnp  26942  efrlim  26946  efrlimOLD  26947  rlimcxp  26951  cxploglim2  26956  emcllem5  26977  zetacvg  26992  lgamgulmlem2  27007  lgamcvg2  27032  0sgmppw  27176  ppiub  27182  chtublem  27189  logfacrlim  27202  logexprlim  27203  chtppilimlem2  27452  rplogsumlem2  27463  dchrisumlem3  27469  dchrvmasumiflem1  27479  dchrisum0lem2  27496  selberg2lem  27528  logdivbnd  27534  pntrsumo1  27543  pntrlog2bndlem4  27558  pntpbnd1  27564  axlowdimlem17  28841  crctcshlem4  29703  clwlkclwwlklem2a1  29874  clwlkclwwlklem2a  29880  clwlkclwwlklem3  29883  clwlkclwwlk  29884  ipidsq  30592  nmcfnexi  31933  sgnsub  34292  knoppndvlem10  36124  poimirlem19  37240  poimirlem20  37241  ftc1anc  37302  cntotbnd  37397  aks4d1p1p2  41670  aks4d1p1p7  41674  posbezout  41700  bcled  41778  irrapxlem3  42383  irrapxlem4  42384  pell14qrgt0  42418  pell1qrgaplem  42432  acongeq  42543  jm2.18  42548  hashnzfz  43896  hashnzfz2  43897  hashnzfzclim  43898  bccn1  43920  binomcxplemnotnn0  43932  dstregt0  44798  absimlere  44997  ellimcabssub0  45140  0ellimcdiv  45172  clim0cf  45177  fprodsubrecnncnvlem  45430  ioodvbdlimc2lem  45457  dvnxpaek  45465  dvnmul  45466  itgsbtaddcnst  45505  stoweidlem7  45530  stoweidlem11  45534  stoweidlem26  45549  dirkertrigeqlem2  45622  fourierdlem57  45686  fourierdlem60  45689  fourierdlem61  45690  fourierdlem68  45697  fourierdlem104  45733  fourierdlem107  45736  fourierdlem109  45738  etransclem4  45761  etransclem23  45780  etransclem27  45784  etransclem31  45788  etransclem35  45792  sigarexp  46382  sigaradd  46389  m1modmmod  47777  dignn0flhalflem1  47871  ehl2eudisval0  47981  2sphere0  48006  line2  48008  line2x  48010  itschlc0yqe  48016  itschlc0xyqsol1  48022  itschlc0xyqsol  48023