Theorem subidd 11555

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  (class class class)co 7405  ℂcc 11104  0cc0 11106   − cmin 11440

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-po 5587  df-so 5588  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-er 8699  df-en 8936  df-dom 8937  df-sdom 8938  df-pnf 11246  df-mnf 11247  df-ltxr 11249  df-sub 11442

This theorem is referenced by:  mulsubaddmulsub  11674  leaddle0  11725  cru  12200  iccf1o  13469  fzocatel  13692  zmod10  13848  hashfzo  14385  hashfzp1  14387  ccatval21sw  14531  ccats1val2  14573  swrd00  14590  ccatpfx  14647  swrdccat3blem  14685  revccat  14712  repswswrd  14730  climconst  15483  rlimconst  15484  telfsumo  15744  fsumparts  15748  incexc  15779  pwdif  15810  cvgrat  15825  binomfallfaclem2  15980  fallfacfac  15985  bpolysum  15993  divalglem5  16336  nn0seqcvgd  16503  pcmpt2  16822  4sqlem15  16888  efgtlen  19588  srgbinomlem3  20044  cayhamlem1  22359  vitalilem1  25116  dvcnp2  25428  dvferm1lem  25492  c1lip1  25505  dv11cn  25509  ftc1lem5  25548  ftc2  25552  plyeq0lem  25715  dgrcolem2  25779  plydivlem4  25800  qaa  25827  aalioulem3  25838  aaliou3lem2  25847  tayl0  25865  dvntaylp  25874  taylthlem1  25876  taylthlem2  25877  abelthlem9  25943  isosctrlem1  26312  birthdaylem2  26446  rlimcnp  26459  lgam1  26557  basellem2  26575  basellem5  26578  chpub  26712  dchrsum2  26760  sumdchr2  26762  2sqmod  26928  rplogsumlem2  26977  dchrisumlem1  26981  pntlemf  27097  colinearalglem4  28156  crctcsh  29067  eucrct2eupth  29487  ipidsq  29950  dip0r  29957  riesz3i  31302  riesz4i  31303  hmopidmpji  31392  pjclem4  31439  pj3si  31447  cycpmco2lem2  32273  cycpmco2lem4  32275  cycpmco2lem6  32277  freshmansdream  32369  fermltlchr  32466  znfermltl  32467  ccfldextdgrr  32734  signsply0  33550  itgexpif  33606  gg-dvcnp2  35162  dnizeq0  35339  unbdqndv2lem2  35374  poimir  36509  itg2addnclem3  36529  ftc1cnnc  36548  ftc2nc  36558  areacirc  36569  sticksstones10  40959  sticksstones12a  40961  metakunt24  40996  lsubcom23d  41188  fltnltalem  41400  3cubeslem2  41408  congid  41695  congabseq  41698  jm2.18  41712  dgrsub2  41862  areaquad  41950  ofsubid  43068  isosctrlem1ALT  43680  supxrgelem  44033  constlimc  44326  ioodvbdlimc1lem1  44633  dvnxpaek  44644  dvnmul  44645  voliooico  44694  voliccico  44701  stoweidlem13  44715  stoweidlem23  44725  stoweidlem26  44728  stirlinglem5  44780  dirkertrigeqlem2  44801  fourierdlem4  44813  fourierdlem42  44851  fourierdlem60  44868  fourierdlem61  44869  fourierdlem74  44882  fourierdlem75  44883  fourierdlem89  44897  fourierdlem90  44898  fourierdlem91  44899  fourierdlem103  44911  fourierdlem104  44912  fourierdlem107  44915  sqwvfoura  44930  etransclem24  44960  etransclem25  44961  hoidmv1lelem1  45293  hoidmv1lelem2  45294  hoidmvlelem1  45297  hoidmvlelem2  45298  volico2  45343  2elfz2melfz  46012  m1mod0mod1  46023  m1modmmod  47160  eenglngeehlnmlem2  47377  rrx2linest  47381  line2x  47393  itscnhlc0yqe  47398  itsclc0yqsollem1  47401