Theorem subidd 11452

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2110  (class class class)co 7341  ℂcc 10996  0cc0 10998   − cmin 11336

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-10 2143  ax-11 2159  ax-12 2179  ax-ext 2702  ax-sep 5232  ax-nul 5242  ax-pow 5301  ax-pr 5368  ax-un 7663  ax-resscn 11055  ax-1cn 11056  ax-icn 11057  ax-addcl 11058  ax-addrcl 11059  ax-mulcl 11060  ax-mulrcl 11061  ax-mulcom 11062  ax-addass 11063  ax-mulass 11064  ax-distr 11065  ax-i2m1 11066  ax-1ne0 11067  ax-1rid 11068  ax-rnegex 11069  ax-rrecex 11070  ax-cnre 11071  ax-pre-lttri 11072  ax-pre-lttrn 11073  ax-pre-ltadd 11074

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-reu 3345  df-rab 3394  df-v 3436  df-sbc 3740  df-csb 3849  df-dif 3903  df-un 3905  df-in 3907  df-ss 3917  df-nul 4282  df-if 4474  df-pw 4550  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4858  df-br 5090  df-opab 5152  df-mpt 5171  df-id 5509  df-po 5522  df-so 5523  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-iota 6433  df-fun 6479  df-fn 6480  df-f 6481  df-f1 6482  df-fo 6483  df-f1o 6484  df-fv 6485  df-riota 7298  df-ov 7344  df-oprab 7345  df-mpo 7346  df-er 8617  df-en 8865  df-dom 8866  df-sdom 8867  df-pnf 11140  df-mnf 11141  df-ltxr 11143  df-sub 11338

This theorem is referenced by:  mulsubaddmulsub  11573  leaddle0  11624  cru  12109  iccf1o  13388  elfzo0suble  13598  fzocatel  13621  zmod10  13783  hashfzo  14328  hashfzp1  14330  ccatval21sw  14485  ccats1val2  14527  swrd00  14544  ccatpfx  14600  swrdccat3blem  14638  revccat  14665  repswswrd  14683  climconst  15442  rlimconst  15443  telfsumo  15701  fsumparts  15705  incexc  15736  pwdif  15767  cvgrat  15782  binomfallfaclem2  15939  fallfacfac  15944  bpolysum  15952  divalglem5  16300  nn0seqcvgd  16473  pcmpt2  16797  4sqlem15  16863  efgtlen  19631  srgbinomlem3  20139  fermltlchr  21459  freshmansdream  21504  cayhamlem1  22774  vitalilem1  25529  dvcnp2  25841  dvcnp2OLD  25842  dvferm1lem  25908  c1lip1  25922  dv11cn  25926  ftc1lem5  25967  ftc2  25971  plyeq0lem  26135  dgrcolem2  26200  plydivlem4  26224  qaa  26251  aalioulem3  26262  aaliou3lem2  26271  tayl0  26289  dvntaylp  26299  taylthlem1  26301  taylthlem2  26302  taylthlem2OLD  26303  abelthlem9  26370  isosctrlem1  26748  birthdaylem2  26882  rlimcnp  26895  lgam1  26994  basellem2  27012  basellem5  27015  chpub  27151  dchrsum2  27199  sumdchr2  27201  2sqmod  27367  rplogsumlem2  27416  dchrisumlem1  27420  pntlemf  27536  colinearalglem4  28880  crctcsh  29795  eucrct2eupth  30215  ipidsq  30680  dip0r  30687  riesz3i  32032  riesz4i  32033  hmopidmpji  32122  pjclem4  32169  pj3si  32177  cycpmco2lem2  33086  cycpmco2lem4  33088  cycpmco2lem6  33090  znfermltl  33321  ccfldextdgrr  33675  constrrtcc  33738  signsply0  34554  itgexpif  34609  dnizeq0  36488  unbdqndv2lem2  36523  poimir  37672  itg2addnclem3  37692  ftc1cnnc  37711  ftc2nc  37721  areacirc  37732  posbezout  42112  aks6d1c5lem1  42148  aks6d1c5lem2  42150  sticksstones10  42167  sticksstones12a  42169  bcle2d  42191  fltnltalem  42674  3cubeslem2  42697  congid  42983  congabseq  42986  jm2.18  43000  dgrsub2  43147  areaquad  43228  ofsubid  44336  isosctrlem1ALT  44945  supxrgelem  45355  constlimc  45643  ioodvbdlimc1lem1  45948  dvnxpaek  45959  dvnmul  45960  voliooico  46009  voliccico  46016  stoweidlem13  46030  stoweidlem23  46040  stoweidlem26  46043  stirlinglem5  46095  dirkertrigeqlem2  46116  fourierdlem4  46128  fourierdlem42  46166  fourierdlem60  46183  fourierdlem61  46184  fourierdlem74  46197  fourierdlem75  46198  fourierdlem89  46212  fourierdlem90  46213  fourierdlem91  46214  fourierdlem103  46226  fourierdlem104  46227  fourierdlem107  46230  sqwvfoura  46245  etransclem24  46275  etransclem25  46276  hoidmv1lelem1  46608  hoidmv1lelem2  46609  hoidmvlelem1  46612  hoidmvlelem2  46613  volico2  46658  2elfz2melfz  47328  m1mod0mod1  47364  m1modmmod  47368  pgnbgreunbgrlem2lem1  48124  pgnbgreunbgrlem2lem2  48125  eenglngeehlnmlem2  48749  rrx2linest  48753  line2x  48765  itscnhlc0yqe  48770  itsclc0yqsollem1  48773