Theorem subidd 11493

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

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

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 5232  ax-nul 5242  ax-pow 5308  ax-pr 5376  ax-un 7689  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 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5526  df-po 5539  df-so 5540  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6455  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-riota 7324  df-ov 7370  df-oprab 7371  df-mpo 7372  df-er 8643  df-en 8894  df-dom 8895  df-sdom 8896  df-pnf 11181  df-mnf 11182  df-ltxr 11184  df-sub 11379

This theorem is referenced by:  mulsubaddmulsub  11614  leaddle0  11665  cru  12151  iccf1o  13449  elfzo0suble  13661  fzocatel  13684  zmod10  13846  hashfzo  14391  hashfzp1  14393  ccatval21sw  14548  ccats1val2  14590  swrd00  14607  ccatpfx  14663  swrdccat3blem  14701  revccat  14728  repswswrd  14746  climconst  15505  rlimconst  15506  telfsumo  15765  fsumparts  15769  incexc  15802  pwdif  15833  cvgrat  15848  binomfallfaclem2  16005  fallfacfac  16010  bpolysum  16018  divalglem5  16366  nn0seqcvgd  16539  pcmpt2  16864  4sqlem15  16930  efgtlen  19701  srgbinomlem3  20209  fermltlchr  21509  freshmansdream  21554  cayhamlem1  22831  vitalilem1  25575  dvcnp2  25887  dvferm1lem  25951  c1lip1  25964  dv11cn  25968  ftc1lem5  26007  ftc2  26011  plyeq0lem  26175  dgrcolem2  26239  plydivlem4  26262  qaa  26289  aalioulem3  26300  aaliou3lem2  26309  tayl0  26327  dvntaylp  26336  taylthlem1  26338  taylthlem2  26339  abelthlem9  26405  isosctrlem1  26782  birthdaylem2  26916  rlimcnp  26929  lgam1  27027  basellem2  27045  basellem5  27048  chpub  27183  dchrsum2  27231  sumdchr2  27233  2sqmod  27399  rplogsumlem2  27448  dchrisumlem1  27452  pntlemf  27568  colinearalglem4  28978  crctcsh  29892  eucrct2eupth  30315  ipidsq  30781  dip0r  30788  riesz3i  32133  riesz4i  32134  hmopidmpji  32223  pjclem4  32270  pj3si  32278  cycpmco2lem2  33188  cycpmco2lem4  33190  cycpmco2lem6  33192  znfermltl  33426  vietalem  33723  ccfldextdgrr  33816  constrrtcc  33879  signsply0  34695  itgexpif  34750  dnizeq0  36735  unbdqndv2lem2  36770  qdiff  37641  poimir  37974  itg2addnclem3  37994  ftc1cnnc  38013  ftc2nc  38023  areacirc  38034  posbezout  42539  aks6d1c5lem1  42575  aks6d1c5lem2  42577  sticksstones10  42594  sticksstones12a  42596  bcle2d  42618  fltnltalem  43095  3cubeslem2  43117  congid  43399  congabseq  43402  jm2.18  43416  dgrsub2  43563  areaquad  43644  ofsubid  44751  isosctrlem1ALT  45360  supxrgelem  45767  constlimc  46054  ioodvbdlimc1lem1  46359  dvnxpaek  46370  dvnmul  46371  voliooico  46420  voliccico  46427  stoweidlem13  46441  stoweidlem23  46451  stoweidlem26  46454  stirlinglem5  46506  dirkertrigeqlem2  46527  fourierdlem4  46539  fourierdlem42  46577  fourierdlem60  46594  fourierdlem61  46595  fourierdlem74  46608  fourierdlem75  46609  fourierdlem89  46623  fourierdlem90  46624  fourierdlem91  46625  fourierdlem103  46637  fourierdlem104  46638  fourierdlem107  46641  sqwvfoura  46656  etransclem24  46686  etransclem25  46687  hoidmv1lelem1  47019  hoidmv1lelem2  47020  hoidmvlelem1  47023  hoidmvlelem2  47024  volico2  47069  2elfz2melfz  47760  m1mod0mod1  47802  m1modmmod  47806  pgnbgreunbgrlem2lem1  48584  pgnbgreunbgrlem2lem2  48585  eenglngeehlnmlem2  49208  rrx2linest  49212  line2x  49224  itscnhlc0yqe  49229  itsclc0yqsollem1  49232