Theorem subidd 10971

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2114  (class class class)co 7142  ℂcc 10521  0cc0 10523   − cmin 10856

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5189  ax-nul 5196  ax-pow 5252  ax-pr 5316  ax-un 7447  ax-resscn 10580  ax-1cn 10581  ax-icn 10582  ax-addcl 10583  ax-addrcl 10584  ax-mulcl 10585  ax-mulrcl 10586  ax-mulcom 10587  ax-addass 10588  ax-mulass 10589  ax-distr 10590  ax-i2m1 10591  ax-1ne0 10592  ax-1rid 10593  ax-rnegex 10594  ax-rrecex 10595  ax-cnre 10596  ax-pre-lttri 10597  ax-pre-lttrn 10598  ax-pre-ltadd 10599

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3488  df-sbc 3764  df-csb 3872  df-dif 3927  df-un 3929  df-in 3931  df-ss 3940  df-nul 4280  df-if 4454  df-pw 4527  df-sn 4554  df-pr 4556  df-op 4560  df-uni 4825  df-br 5053  df-opab 5115  df-mpt 5133  df-id 5446  df-po 5460  df-so 5461  df-xp 5547  df-rel 5548  df-cnv 5549  df-co 5550  df-dm 5551  df-rn 5552  df-res 5553  df-ima 5554  df-iota 6300  df-fun 6343  df-fn 6344  df-f 6345  df-f1 6346  df-fo 6347  df-f1o 6348  df-fv 6349  df-riota 7100  df-ov 7145  df-oprab 7146  df-mpo 7147  df-er 8275  df-en 8496  df-dom 8497  df-sdom 8498  df-pnf 10663  df-mnf 10664  df-ltxr 10666  df-sub 10858

This theorem is referenced by:  mulsubaddmulsub  11090  leaddle0  11141  cru  11616  iccf1o  12871  fzocatel  13091  zmod10  13245  hashfzo  13780  hashfzp1  13782  ccatval21sw  13924  ccats1val2  13968  swrd00  13991  ccatpfx  14048  swrdccat3blem  14086  revccat  14113  repswswrd  14131  climconst  14885  rlimconst  14886  telfsumo  15142  fsumparts  15146  incexc  15177  pwdif  15208  cvgrat  15224  binomfallfaclem2  15379  fallfacfac  15384  bpolysum  15392  divalglem5  15731  nn0seqcvgd  15897  pcmpt2  16212  4sqlem15  16278  efgtlen  18835  srgbinomlem3  19275  cayhamlem1  21457  vitalilem1  24192  dvcnp2  24502  dvferm1lem  24566  c1lip1  24579  dv11cn  24583  ftc1lem5  24622  ftc2  24626  plyeq0lem  24786  dgrcolem2  24850  plydivlem4  24871  qaa  24898  aalioulem3  24909  aaliou3lem2  24918  tayl0  24936  dvntaylp  24945  taylthlem1  24947  taylthlem2  24948  abelthlem9  25014  isosctrlem1  25382  birthdaylem2  25516  rlimcnp  25529  lgam1  25627  basellem2  25645  basellem5  25648  chpub  25782  dchrsum2  25830  sumdchr2  25832  2sqmod  25998  rplogsumlem2  26047  dchrisumlem1  26051  pntlemf  26167  colinearalglem4  26681  crctcsh  27588  eucrct2eupth  28008  ipidsq  28471  dip0r  28478  riesz3i  29823  riesz4i  29824  hmopidmpji  29913  pjclem4  29960  pj3si  29968  cycpmco2lem2  30776  cycpmco2lem4  30778  cycpmco2lem6  30780  freshmansdream  30866  ccfldextdgrr  31067  signsply0  31828  itgexpif  31884  dnizeq0  33821  unbdqndv2lem2  33856  poimir  34959  itg2addnclem3  34979  ftc1cnnc  34998  ftc2nc  35008  areacirc  35019  fltnltalem  39366  3cubeslem2  39374  congid  39660  congabseq  39663  jm2.18  39677  dgrsub2  39827  areaquad  39914  ofsubid  40746  isosctrlem1ALT  41358  supxrgelem  41695  constlimc  41995  ioodvbdlimc1lem1  42306  dvnxpaek  42317  dvnmul  42318  voliooico  42367  voliccico  42374  stoweidlem13  42388  stoweidlem23  42398  stoweidlem26  42401  stirlinglem5  42453  dirkertrigeqlem2  42474  fourierdlem4  42486  fourierdlem42  42524  fourierdlem60  42541  fourierdlem61  42542  fourierdlem74  42555  fourierdlem75  42556  fourierdlem89  42570  fourierdlem90  42571  fourierdlem91  42572  fourierdlem103  42584  fourierdlem104  42585  fourierdlem107  42588  sqwvfoura  42603  etransclem24  42633  etransclem25  42634  hoidmv1lelem1  42963  hoidmv1lelem2  42964  hoidmvlelem1  42967  hoidmvlelem2  42968  volico2  43013  2elfz2melfz  43608  m1mod0mod1  43619  m1modmmod  44666  eenglngeehlnmlem2  44810  rrx2linest  44814  line2x  44826  itscnhlc0yqe  44831  itsclc0yqsollem1  44834