Theorem subidd 11492

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7368  ℂcc 11036  0cc0 11038   − cmin 11376

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-po 5540  df-so 5541  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-riota 7325  df-ov 7371  df-oprab 7372  df-mpo 7373  df-er 8645  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11180  df-mnf 11181  df-ltxr 11183  df-sub 11378

This theorem is referenced by:  mulsubaddmulsub  11613  leaddle0  11664  cru  12149  iccf1o  13424  elfzo0suble  13634  fzocatel  13657  zmod10  13819  hashfzo  14364  hashfzp1  14366  ccatval21sw  14521  ccats1val2  14563  swrd00  14580  ccatpfx  14636  swrdccat3blem  14674  revccat  14701  repswswrd  14719  climconst  15478  rlimconst  15479  telfsumo  15737  fsumparts  15741  incexc  15772  pwdif  15803  cvgrat  15818  binomfallfaclem2  15975  fallfacfac  15980  bpolysum  15988  divalglem5  16336  nn0seqcvgd  16509  pcmpt2  16833  4sqlem15  16899  efgtlen  19667  srgbinomlem3  20175  fermltlchr  21496  freshmansdream  21541  cayhamlem1  22822  vitalilem1  25577  dvcnp2  25889  dvcnp2OLD  25890  dvferm1lem  25956  c1lip1  25970  dv11cn  25974  ftc1lem5  26015  ftc2  26019  plyeq0lem  26183  dgrcolem2  26248  plydivlem4  26272  qaa  26299  aalioulem3  26310  aaliou3lem2  26319  tayl0  26337  dvntaylp  26347  taylthlem1  26349  taylthlem2  26350  taylthlem2OLD  26351  abelthlem9  26418  isosctrlem1  26796  birthdaylem2  26930  rlimcnp  26943  lgam1  27042  basellem2  27060  basellem5  27063  chpub  27199  dchrsum2  27247  sumdchr2  27249  2sqmod  27415  rplogsumlem2  27464  dchrisumlem1  27468  pntlemf  27584  colinearalglem4  28994  crctcsh  29909  eucrct2eupth  30332  ipidsq  30797  dip0r  30804  riesz3i  32149  riesz4i  32150  hmopidmpji  32239  pjclem4  32286  pj3si  32294  cycpmco2lem2  33220  cycpmco2lem4  33222  cycpmco2lem6  33224  znfermltl  33458  vietalem  33755  ccfldextdgrr  33849  constrrtcc  33912  signsply0  34728  itgexpif  34783  dnizeq0  36694  unbdqndv2lem2  36729  poimir  37893  itg2addnclem3  37913  ftc1cnnc  37932  ftc2nc  37942  areacirc  37953  posbezout  42459  aks6d1c5lem1  42495  aks6d1c5lem2  42497  sticksstones10  42514  sticksstones12a  42516  bcle2d  42538  fltnltalem  43009  3cubeslem2  43031  congid  43317  congabseq  43320  jm2.18  43334  dgrsub2  43481  areaquad  43562  ofsubid  44669  isosctrlem1ALT  45278  supxrgelem  45685  constlimc  45973  ioodvbdlimc1lem1  46278  dvnxpaek  46289  dvnmul  46290  voliooico  46339  voliccico  46346  stoweidlem13  46360  stoweidlem23  46370  stoweidlem26  46373  stirlinglem5  46425  dirkertrigeqlem2  46446  fourierdlem4  46458  fourierdlem42  46496  fourierdlem60  46513  fourierdlem61  46514  fourierdlem74  46527  fourierdlem75  46528  fourierdlem89  46542  fourierdlem90  46543  fourierdlem91  46544  fourierdlem103  46556  fourierdlem104  46557  fourierdlem107  46560  sqwvfoura  46575  etransclem24  46605  etransclem25  46606  hoidmv1lelem1  46938  hoidmv1lelem2  46939  hoidmvlelem1  46942  hoidmvlelem2  46943  volico2  46988  2elfz2melfz  47667  m1mod0mod1  47703  m1modmmod  47707  pgnbgreunbgrlem2lem1  48463  pgnbgreunbgrlem2lem2  48464  eenglngeehlnmlem2  49087  rrx2linest  49091  line2x  49103  itscnhlc0yqe  49108  itsclc0yqsollem1  49111