Theorem subidd 11023

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

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111  (class class class)co 7150  ℂcc 10573  0cc0 10575   − cmin 10908

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5169  ax-nul 5176  ax-pow 5234  ax-pr 5298  ax-un 7459  ax-resscn 10632  ax-1cn 10633  ax-icn 10634  ax-addcl 10635  ax-addrcl 10636  ax-mulcl 10637  ax-mulrcl 10638  ax-mulcom 10639  ax-addass 10640  ax-mulass 10641  ax-distr 10642  ax-i2m1 10643  ax-1ne0 10644  ax-1rid 10645  ax-rnegex 10646  ax-rrecex 10647  ax-cnre 10648  ax-pre-lttri 10649  ax-pre-lttrn 10650  ax-pre-ltadd 10651

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-nel 3056  df-ral 3075  df-rex 3076  df-reu 3077  df-rab 3079  df-v 3411  df-sbc 3697  df-csb 3806  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-nul 4226  df-if 4421  df-pw 4496  df-sn 4523  df-pr 4525  df-op 4529  df-uni 4799  df-br 5033  df-opab 5095  df-mpt 5113  df-id 5430  df-po 5443  df-so 5444  df-xp 5530  df-rel 5531  df-cnv 5532  df-co 5533  df-dm 5534  df-rn 5535  df-res 5536  df-ima 5537  df-iota 6294  df-fun 6337  df-fn 6338  df-f 6339  df-f1 6340  df-fo 6341  df-f1o 6342  df-fv 6343  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-er 8299  df-en 8528  df-dom 8529  df-sdom 8530  df-pnf 10715  df-mnf 10716  df-ltxr 10718  df-sub 10910

This theorem is referenced by:  mulsubaddmulsub  11142  leaddle0  11193  cru  11666  iccf1o  12928  fzocatel  13150  zmod10  13304  hashfzo  13840  hashfzp1  13842  ccatval21sw  13986  ccats1val2  14030  swrd00  14053  ccatpfx  14110  swrdccat3blem  14148  revccat  14175  repswswrd  14193  climconst  14948  rlimconst  14949  telfsumo  15205  fsumparts  15209  incexc  15240  pwdif  15271  cvgrat  15287  binomfallfaclem2  15442  fallfacfac  15447  bpolysum  15455  divalglem5  15798  nn0seqcvgd  15966  pcmpt2  16284  4sqlem15  16350  efgtlen  18919  srgbinomlem3  19360  cayhamlem1  21566  vitalilem1  24308  dvcnp2  24619  dvferm1lem  24683  c1lip1  24696  dv11cn  24700  ftc1lem5  24739  ftc2  24743  plyeq0lem  24906  dgrcolem2  24970  plydivlem4  24991  qaa  25018  aalioulem3  25029  aaliou3lem2  25038  tayl0  25056  dvntaylp  25065  taylthlem1  25067  taylthlem2  25068  abelthlem9  25134  isosctrlem1  25503  birthdaylem2  25637  rlimcnp  25650  lgam1  25748  basellem2  25766  basellem5  25769  chpub  25903  dchrsum2  25951  sumdchr2  25953  2sqmod  26119  rplogsumlem2  26168  dchrisumlem1  26172  pntlemf  26288  colinearalglem4  26802  crctcsh  27709  eucrct2eupth  28129  ipidsq  28592  dip0r  28599  riesz3i  29944  riesz4i  29945  hmopidmpji  30034  pjclem4  30081  pj3si  30089  cycpmco2lem2  30920  cycpmco2lem4  30922  cycpmco2lem6  30924  freshmansdream  31010  znfermltl  31083  ccfldextdgrr  31263  signsply0  32049  itgexpif  32105  dnizeq0  34226  unbdqndv2lem2  34261  poimir  35392  itg2addnclem3  35412  ftc1cnnc  35431  ftc2nc  35441  areacirc  35452  metakunt24  39692  lsubcom23d  39831  fltnltalem  40013  3cubeslem2  40021  congid  40307  congabseq  40310  jm2.18  40324  dgrsub2  40474  areaquad  40561  ofsubid  41423  isosctrlem1ALT  42035  supxrgelem  42359  constlimc  42654  ioodvbdlimc1lem1  42961  dvnxpaek  42972  dvnmul  42973  voliooico  43022  voliccico  43029  stoweidlem13  43043  stoweidlem23  43053  stoweidlem26  43056  stirlinglem5  43108  dirkertrigeqlem2  43129  fourierdlem4  43141  fourierdlem42  43179  fourierdlem60  43196  fourierdlem61  43197  fourierdlem74  43210  fourierdlem75  43211  fourierdlem89  43225  fourierdlem90  43226  fourierdlem91  43227  fourierdlem103  43239  fourierdlem104  43240  fourierdlem107  43243  sqwvfoura  43258  etransclem24  43288  etransclem25  43289  hoidmv1lelem1  43618  hoidmv1lelem2  43619  hoidmvlelem1  43622  hoidmvlelem2  43623  volico2  43668  2elfz2melfz  44265  m1mod0mod1  44276  m1modmmod  45322  eenglngeehlnmlem2  45539  rrx2linest  45543  line2x  45555  itscnhlc0yqe  45560  itsclc0yqsollem1  45563