Theorem subidd 10839

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

Syntax hints:   → wi 4   = wceq 1525   ∈ wcel 2083  (class class class)co 7023  ℂcc 10388  0cc0 10390   − cmin 10723

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-13 2346  ax-ext 2771  ax-sep 5101  ax-nul 5108  ax-pow 5164  ax-pr 5228  ax-un 7326  ax-resscn 10447  ax-1cn 10448  ax-icn 10449  ax-addcl 10450  ax-addrcl 10451  ax-mulcl 10452  ax-mulrcl 10453  ax-mulcom 10454  ax-addass 10455  ax-mulass 10456  ax-distr 10457  ax-i2m1 10458  ax-1ne0 10459  ax-1rid 10460  ax-rnegex 10461  ax-rrecex 10462  ax-cnre 10463  ax-pre-lttri 10464  ax-pre-lttrn 10465  ax-pre-ltadd 10466

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-mo 2578  df-eu 2614  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ne 2987  df-nel 3093  df-ral 3112  df-rex 3113  df-reu 3114  df-rab 3116  df-v 3442  df-sbc 3712  df-csb 3818  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-nul 4218  df-if 4388  df-pw 4461  df-sn 4479  df-pr 4481  df-op 4485  df-uni 4752  df-br 4969  df-opab 5031  df-mpt 5048  df-id 5355  df-po 5369  df-so 5370  df-xp 5456  df-rel 5457  df-cnv 5458  df-co 5459  df-dm 5460  df-rn 5461  df-res 5462  df-ima 5463  df-iota 6196  df-fun 6234  df-fn 6235  df-f 6236  df-f1 6237  df-fo 6238  df-f1o 6239  df-fv 6240  df-riota 6984  df-ov 7026  df-oprab 7027  df-mpo 7028  df-er 8146  df-en 8365  df-dom 8366  df-sdom 8367  df-pnf 10530  df-mnf 10531  df-ltxr 10533  df-sub 10725

This theorem is referenced by:  mulsubaddmulsub  10958  leaddle0  11009  cru  11484  iccf1o  12736  fzocatel  12955  zmod10  13109  hashfzo  13642  hashfzp1  13644  ccatval21sw  13787  ccats1val2  13829  swrd00  13846  ccatpfx  13903  swrdccat3blem  13941  revccat  13968  repswswrd  13986  climconst  14738  rlimconst  14739  telfsumo  14994  fsumparts  14998  incexc  15029  pwdif  15060  cvgrat  15076  binomfallfaclem2  15231  fallfacfac  15236  bpolysum  15244  divalglem5  15585  nn0seqcvgd  15747  pcmpt2  16062  4sqlem15  16128  efgtlen  18583  srgbinomlem3  18986  cayhamlem1  21162  vitalilem1  23896  dvcnp2  24204  dvferm1lem  24268  c1lip1  24281  dv11cn  24285  ftc1lem5  24324  ftc2  24328  plyeq0lem  24487  dgrcolem2  24551  plydivlem4  24572  qaa  24599  aalioulem3  24610  aaliou3lem2  24619  tayl0  24637  dvntaylp  24646  taylthlem1  24648  taylthlem2  24649  abelthlem9  24715  isosctrlem1  25081  birthdaylem2  25216  rlimcnp  25229  lgam1  25327  basellem2  25345  basellem5  25348  chpub  25482  dchrsum2  25530  sumdchr2  25532  2sqmod  25698  rplogsumlem2  25747  dchrisumlem1  25751  pntlemf  25867  colinearalglem4  26382  crctcsh  27288  eucrct2eupth  27710  ipidsq  28174  dip0r  28181  riesz3i  29526  riesz4i  29527  hmopidmpji  29616  pjclem4  29663  pj3si  29671  freshmansdream  30509  ccfldextdgrr  30657  signsply0  31434  itgexpif  31490  dnizeq0  33425  unbdqndv2lem2  33460  poimir  34477  itg2addnclem3  34497  ftc1cnnc  34518  ftc2nc  34528  areacirc  34539  fltnltalem  38792  congid  39074  congabseq  39077  jm2.18  39091  dgrsub2  39241  areaquad  39329  ofsubid  40215  isosctrlem1ALT  40828  supxrgelem  41167  constlimc  41468  ioodvbdlimc1lem1  41779  dvnxpaek  41790  dvnmul  41791  voliooico  41841  voliccico  41848  stoweidlem13  41862  stoweidlem23  41872  stoweidlem26  41875  stirlinglem5  41927  dirkertrigeqlem2  41948  fourierdlem4  41960  fourierdlem42  41998  fourierdlem60  42015  fourierdlem61  42016  fourierdlem74  42029  fourierdlem75  42030  fourierdlem89  42044  fourierdlem90  42045  fourierdlem91  42046  fourierdlem103  42058  fourierdlem104  42059  fourierdlem107  42062  sqwvfoura  42077  etransclem24  42107  etransclem25  42108  hoidmv1lelem1  42437  hoidmv1lelem2  42438  hoidmvlelem1  42441  hoidmvlelem2  42442  volico2  42487  2elfz2melfz  43056  m1mod0mod1  43067  m1modmmod  44084  eenglngeehlnmlem2  44228  rrx2linest  44232  line2x  44244  itscnhlc0yqe  44249  itsclc0yqsollem1  44252