Theorem subidd 11584

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  (class class class)co 7416  ℂcc 11125  0cc0 11127   − cmin 11468

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7739  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-mulcom 11191  ax-addass 11192  ax-mulass 11193  ax-distr 11194  ax-i2m1 11195  ax-1ne0 11196  ax-1rid 11197  ax-rnegex 11198  ax-rrecex 11199  ax-cnre 11200  ax-pre-lttri 11201  ax-pre-lttrn 11202  ax-pre-ltadd 11203

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-po 5567  df-so 5568  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7373  df-ov 7419  df-oprab 7420  df-mpo 7421  df-er 8699  df-en 8956  df-dom 8957  df-sdom 8958  df-pnf 11272  df-mnf 11273  df-ltxr 11275  df-sub 11470

This theorem is used by:  mulsubaddmulsub  11705  leaddle0  11756  cru  12237  iccf1o  13551  elfzo0suble  13764  fzocatel  13787  zmod10  13950  hashfzo  14496  hashfzp1  14498  ccatval21sw  14653  ccats1val2  14697  swrd00  14714  ccatpfx  14772  swrdccat3blem  14810  revccat  14837  repswswrd  14857  climconst  15632  rlimconst  15633  telfsumo  15891  fsumparts  15895  incexc  15928  pwdif  15959  cvgrat  15974  binomfallfaclem2  16130  fallfacfac  16135  bpolysum  16143  divalglem5  16491  nn0seqcvgd  16664  pcmpt2  16989  4sqlem15  17055  efgtlen  19857  srgbinomlem3  20371  fermltlchr  21746  freshmansdream  21791  cayhamlem1  23095  vitalilem1  25840  dvcnp2  26152  dvferm1lem  26216  c1lip1  26229  dv11cn  26233  ftc1lem5  26272  ftc2  26276  plyeq0lem  26440  dgrcolem2  26504  plydivlem4  26530  qaa  26557  aalioulem3  26570  aaliou3lem2  26579  tayl0  26598  dvntaylp  26607  taylthlem1  26609  taylthlem2  26610  abelthlem9  26676  isosctrlem1  27056  birthdaylem2  27190  rlimcnp  27203  lgam1  27301  basellem2  27319  basellem5  27322  chpub  27457  dchrsum2  27505  sumdchr2  27507  2sqmod  27673  rplogsumlem2  27722  dchrisumlem1  27726  pntlemf  27842  colinearalglem4  29367  crctcsh  30293  eucrct2eupth  30726  ipidsq  31192  dip0r  31199  riesz3i  32544  riesz4i  32545  hmopidmpji  32634  pjclem4  32681  pj3si  32689  cycpmco2lem2  33569  cycpmco2lem4  33571  cycpmco2lem6  33573  znfermltl  33803  vietalem  34091  ccfldextdgrr  34184  constrrtcc  34247  signsply0  35061  itgexpif  35116  dnizeq0  37174  unbdqndv2lem2  37209  qdiff  38081  poimir  38404  itg2addnclem3  38424  ftc1cnnc  38443  ftc2nc  38453  areacirc  38464  posbezout  42968  aks6d1c5lem1  43004  aks6d1c5lem2  43006  sticksstones10  43023  sticksstones12a  43025  bcle2d  43047  fltnltalem  43510  3cubeslem2  43532  congid  43814  congabseq  43817  jm2.18  43831  dgrsub2  43978  areaquad  44059  ofsubid  45150  isosctrlem1ALT  45758  supxrgelem  46169  constlimc  46456  ioodvbdlimc1lem1  46761  dvnxpaek  46772  dvnmul  46773  voliooico  46822  voliccico  46829  stoweidlem13  46843  stoweidlem23  46853  stoweidlem26  46856  stirlinglem5  46908  dirkertrigeqlem2  46929  fourierdlem4  46941  fourierdlem42  46979  fourierdlem60  46996  fourierdlem61  46997  fourierdlem74  47010  fourierdlem75  47011  fourierdlem89  47025  fourierdlem90  47026  fourierdlem91  47027  fourierdlem103  47039  fourierdlem104  47040  fourierdlem107  47043  sqwvfoura  47058  etransclem24  47088  etransclem25  47089  hoidmv1lelem1  47421  hoidmv1lelem2  47422  hoidmvlelem1  47425  hoidmvlelem2  47426  volico2  47471  sqrtnnaa  47733  2elfz2melfz  48208  m1mod0mod1  48250  m1modmmod  48254  pgnbgreunbgrlem2lem1  49032  pgnbgreunbgrlem2lem2  49033  eenglngeehlnmlem2  49670  rrx2linest  49674  line2x  49686  itscnhlc0yqe  49691  itsclc0yqsollem1  49694