Theorem subidd 11250

Description: Subtraction of a number from itself. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
negidd.1	⊢ (𝜑 → 𝐴 ∈ ℂ)

Assertion

Ref	Expression
subidd	⊢ (𝜑 → (𝐴 − 𝐴) = 0)

Proof of Theorem subidd

Step	Hyp	Ref	Expression
1		negidd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		subid 11170	. 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:  mulsubaddmulsub  11369  leaddle0  11420  cru  11895  iccf1o  13157  fzocatel  13379  zmod10  13535  hashfzo  14072  hashfzp1  14074  ccatval21sw  14218  ccats1val2  14262  swrd00  14285  ccatpfx  14342  swrdccat3blem  14380  revccat  14407  repswswrd  14425  climconst  15180  rlimconst  15181  telfsumo  15442  fsumparts  15446  incexc  15477  pwdif  15508  cvgrat  15523  binomfallfaclem2  15678  fallfacfac  15683  bpolysum  15691  divalglem5  16034  nn0seqcvgd  16203  pcmpt2  16522  4sqlem15  16588  efgtlen  19247  srgbinomlem3  19693  cayhamlem1  21923  vitalilem1  24677  dvcnp2  24989  dvferm1lem  25053  c1lip1  25066  dv11cn  25070  ftc1lem5  25109  ftc2  25113  plyeq0lem  25276  dgrcolem2  25340  plydivlem4  25361  qaa  25388  aalioulem3  25399  aaliou3lem2  25408  tayl0  25426  dvntaylp  25435  taylthlem1  25437  taylthlem2  25438  abelthlem9  25504  isosctrlem1  25873  birthdaylem2  26007  rlimcnp  26020  lgam1  26118  basellem2  26136  basellem5  26139  chpub  26273  dchrsum2  26321  sumdchr2  26323  2sqmod  26489  rplogsumlem2  26538  dchrisumlem1  26542  pntlemf  26658  colinearalglem4  27180  crctcsh  28090  eucrct2eupth  28510  ipidsq  28973  dip0r  28980  riesz3i  30325  riesz4i  30326  hmopidmpji  30415  pjclem4  30462  pj3si  30470  cycpmco2lem2  31296  cycpmco2lem4  31298  cycpmco2lem6  31300  freshmansdream  31386  znfermltl  31464  ccfldextdgrr  31644  signsply0  32430  itgexpif  32486  dnizeq0  34582  unbdqndv2lem2  34617  poimir  35737  itg2addnclem3  35757  ftc1cnnc  35776  ftc2nc  35786  areacirc  35797  sticksstones10  40039  sticksstones12a  40041  metakunt24  40076  lsubcom23d  40228  fltnltalem  40415  3cubeslem2  40423  congid  40709  congabseq  40712  jm2.18  40726  dgrsub2  40876  areaquad  40963  ofsubid  41831  isosctrlem1ALT  42443  supxrgelem  42766  constlimc  43055  ioodvbdlimc1lem1  43362  dvnxpaek  43373  dvnmul  43374  voliooico  43423  voliccico  43430  stoweidlem13  43444  stoweidlem23  43454  stoweidlem26  43457  stirlinglem5  43509  dirkertrigeqlem2  43530  fourierdlem4  43542  fourierdlem42  43580  fourierdlem60  43597  fourierdlem61  43598  fourierdlem74  43611  fourierdlem75  43612  fourierdlem89  43626  fourierdlem90  43627  fourierdlem91  43628  fourierdlem103  43640  fourierdlem104  43641  fourierdlem107  43644  sqwvfoura  43659  etransclem24  43689  etransclem25  43690  hoidmv1lelem1  44019  hoidmv1lelem2  44020  hoidmvlelem1  44023  hoidmvlelem2  44024  volico2  44069  2elfz2melfz  44698  m1mod0mod1  44709  m1modmmod  45755  eenglngeehlnmlem2  45972  rrx2linest  45976  line2x  45988  itscnhlc0yqe  45993  itsclc0yqsollem1  45996