Theorem subidd 11610

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

Syntax hints:   → wi 4   = wceq 1534   ∈ wcel 2100  (class class class)co 7427  ℂcc 11157  0cc0 11159   − cmin 11495

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2102  ax-9 2110  ax-10 2133  ax-11 2150  ax-12 2170  ax-ext 2700  ax-sep 5305  ax-nul 5312  ax-pow 5371  ax-pr 5435  ax-un 7748  ax-resscn 11216  ax-1cn 11217  ax-icn 11218  ax-addcl 11219  ax-addrcl 11220  ax-mulcl 11221  ax-mulrcl 11222  ax-mulcom 11223  ax-addass 11224  ax-mulass 11225  ax-distr 11226  ax-i2m1 11227  ax-1ne0 11228  ax-1rid 11229  ax-rnegex 11230  ax-rrecex 11231  ax-cnre 11232  ax-pre-lttri 11233  ax-pre-lttrn 11234  ax-pre-ltadd 11235

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2062  df-mo 2532  df-eu 2561  df-clab 2707  df-cleq 2721  df-clel 2806  df-nfc 2881  df-ne 2934  df-nel 3040  df-ral 3055  df-rex 3064  df-reu 3374  df-rab 3429  df-v 3474  df-sbc 3788  df-csb 3904  df-dif 3961  df-un 3963  df-in 3965  df-ss 3975  df-nul 4334  df-if 4535  df-pw 4610  df-sn 4635  df-pr 4637  df-op 4641  df-uni 4917  df-br 5155  df-opab 5217  df-mpt 5238  df-id 5582  df-po 5596  df-so 5597  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-iota 6508  df-fun 6558  df-fn 6559  df-f 6560  df-f1 6561  df-fo 6562  df-f1o 6563  df-fv 6564  df-riota 7383  df-ov 7430  df-oprab 7431  df-mpo 7432  df-er 8738  df-en 8979  df-dom 8980  df-sdom 8981  df-pnf 11301  df-mnf 11302  df-ltxr 11304  df-sub 11497

This theorem is referenced by:  mulsubaddmulsub  11729  leaddle0  11780  cru  12260  iccf1o  13531  fzocatel  13754  zmod10  13912  hashfzo  14452  hashfzp1  14454  ccatval21sw  14606  ccats1val2  14648  swrd00  14665  ccatpfx  14722  swrdccat3blem  14760  revccat  14787  repswswrd  14805  climconst  15558  rlimconst  15559  telfsumo  15819  fsumparts  15823  incexc  15854  pwdif  15885  cvgrat  15900  binomfallfaclem2  16055  fallfacfac  16060  bpolysum  16068  divalglem5  16412  nn0seqcvgd  16584  pcmpt2  16908  4sqlem15  16974  efgtlen  19736  srgbinomlem3  20223  fermltlchr  21535  freshmansdream  21584  cayhamlem1  22859  vitalilem1  25628  dvcnp2  25940  dvcnp2OLD  25941  dvferm1lem  26007  c1lip1  26021  dv11cn  26025  ftc1lem5  26066  ftc2  26070  plyeq0lem  26234  dgrcolem2  26299  plydivlem4  26321  qaa  26348  aalioulem3  26359  aaliou3lem2  26368  tayl0  26386  dvntaylp  26396  taylthlem1  26398  taylthlem2  26399  taylthlem2OLD  26400  abelthlem9  26467  isosctrlem1  26843  birthdaylem2  26977  rlimcnp  26990  lgam1  27089  basellem2  27107  basellem5  27110  chpub  27246  dchrsum2  27294  sumdchr2  27296  2sqmod  27462  rplogsumlem2  27511  dchrisumlem1  27515  pntlemf  27631  colinearalglem4  28885  crctcsh  29800  eucrct2eupth  30220  ipidsq  30685  dip0r  30692  riesz3i  32037  riesz4i  32038  hmopidmpji  32127  pjclem4  32174  pj3si  32182  cycpmco2lem2  33065  cycpmco2lem4  33067  cycpmco2lem6  33069  znfermltl  33304  ccfldextdgrr  33627  constrrtcc  33671  signsply0  34473  itgexpif  34528  dnizeq0  36264  unbdqndv2lem2  36299  poimir  37439  itg2addnclem3  37459  ftc1cnnc  37478  ftc2nc  37488  areacirc  37499  posbezout  41884  aks6d1c5lem1  41920  aks6d1c5lem2  41922  sticksstones10  41939  sticksstones12a  41941  bcle2d  41963  metakunt24  42011  lsubswap23d  42093  fltnltalem  42427  3cubeslem2  42454  congid  42741  congabseq  42744  jm2.18  42758  dgrsub2  42908  areaquad  42993  ofsubid  44110  isosctrlem1ALT  44722  supxrgelem  45063  constlimc  45356  ioodvbdlimc1lem1  45663  dvnxpaek  45674  dvnmul  45675  voliooico  45724  voliccico  45731  stoweidlem13  45745  stoweidlem23  45755  stoweidlem26  45758  stirlinglem5  45810  dirkertrigeqlem2  45831  fourierdlem4  45843  fourierdlem42  45881  fourierdlem60  45898  fourierdlem61  45899  fourierdlem74  45912  fourierdlem75  45913  fourierdlem89  45927  fourierdlem90  45928  fourierdlem91  45929  fourierdlem103  45941  fourierdlem104  45942  fourierdlem107  45945  sqwvfoura  45960  etransclem24  45990  etransclem25  45991  hoidmv1lelem1  46323  hoidmv1lelem2  46324  hoidmvlelem1  46327  hoidmvlelem2  46328  volico2  46373  2elfz2melfz  47042  m1mod0mod1  47052  m1modmmod  48031  eenglngeehlnmlem2  48248  rrx2linest  48252  line2x  48264  itscnhlc0yqe  48269  itsclc0yqsollem1  48272