Theorem subidd 11556

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

Syntax hints:   → wi 4   = wceq 1568   ∈ wcel 2141  (class class class)co 7410  ℂcc 11097  0cc0 11099   − cmin 11440

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5256  ax-nul 5268  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-resscn 11156  ax-1cn 11157  ax-icn 11158  ax-addcl 11159  ax-addrcl 11160  ax-mulcl 11161  ax-mulrcl 11162  ax-mulcom 11163  ax-addass 11164  ax-mulass 11165  ax-distr 11166  ax-i2m1 11167  ax-1ne0 11168  ax-1rid 11169  ax-rnegex 11170  ax-rrecex 11171  ax-cnre 11172  ax-pre-lttri 11173  ax-pre-lttrn 11174  ax-pre-ltadd 11175

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-nf 1812  df-sb 2095  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3744  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-pw 4563  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-opab 5173  df-mpt 5192  df-id 5556  df-po 5569  df-so 5570  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-er 8693  df-en 8943  df-dom 8944  df-sdom 8945  df-pnf 11244  df-mnf 11245  df-ltxr 11247  df-sub 11442

This theorem is referenced by:  mulsubaddmulsub  11677  leaddle0  11728  cru  12209  iccf1o  13522  elfzo0suble  13735  fzocatel  13758  zmod10  13920  hashfzo  14466  hashfzp1  14468  ccatval21sw  14623  ccats1val2  14665  swrd00  14682  ccatpfx  14738  swrdccat3blem  14776  revccat  14803  repswswrd  14821  climconst  15594  rlimconst  15595  telfsumo  15854  fsumparts  15858  incexc  15891  pwdif  15922  cvgrat  15937  binomfallfaclem2  16093  fallfacfac  16098  bpolysum  16106  divalglem5  16454  nn0seqcvgd  16627  pcmpt2  16952  4sqlem15  17018  efgtlen  19795  srgbinomlem3  20309  fermltlchr  21658  freshmansdream  21703  cayhamlem1  23002  vitalilem1  25746  dvcnp2  26058  dvferm1lem  26122  c1lip1  26135  dv11cn  26139  ftc1lem5  26178  ftc2  26182  plyeq0lem  26346  dgrcolem2  26410  plydivlem4  26436  qaa  26463  aalioulem3  26474  aaliou3lem2  26483  tayl0  26501  dvntaylp  26510  taylthlem1  26512  taylthlem2  26513  abelthlem9  26579  isosctrlem1  26959  birthdaylem2  27093  rlimcnp  27106  lgam1  27204  basellem2  27222  basellem5  27225  chpub  27360  dchrsum2  27408  sumdchr2  27410  2sqmod  27576  rplogsumlem2  27625  dchrisumlem1  27629  pntlemf  27745  colinearalglem4  29225  crctcsh  30139  eucrct2eupth  30562  ipidsq  31028  dip0r  31035  riesz3i  32380  riesz4i  32381  hmopidmpji  32470  pjclem4  32517  pj3si  32525  cycpmco2lem2  33413  cycpmco2lem4  33415  cycpmco2lem6  33417  znfermltl  33647  vietalem  33935  ccfldextdgrr  34028  constrrtcc  34091  signsply0  34904  itgexpif  34959  dnizeq0  37030  unbdqndv2lem2  37065  qdiff  37937  poimir  38270  itg2addnclem3  38290  ftc1cnnc  38309  ftc2nc  38319  areacirc  38330  posbezout  42835  aks6d1c5lem1  42871  aks6d1c5lem2  42873  sticksstones10  42890  sticksstones12a  42892  bcle2d  42914  fltnltalem  43364  3cubeslem2  43386  congid  43668  congabseq  43671  jm2.18  43685  dgrsub2  43832  areaquad  43913  ofsubid  45004  isosctrlem1ALT  45612  supxrgelem  46023  constlimc  46310  ioodvbdlimc1lem1  46615  dvnxpaek  46626  dvnmul  46627  voliooico  46676  voliccico  46683  stoweidlem13  46697  stoweidlem23  46707  stoweidlem26  46710  stirlinglem5  46762  dirkertrigeqlem2  46783  fourierdlem4  46795  fourierdlem42  46833  fourierdlem60  46850  fourierdlem61  46851  fourierdlem74  46864  fourierdlem75  46865  fourierdlem89  46879  fourierdlem90  46880  fourierdlem91  46881  fourierdlem103  46893  fourierdlem104  46894  fourierdlem107  46897  sqwvfoura  46912  etransclem24  46942  etransclem25  46943  hoidmv1lelem1  47275  hoidmv1lelem2  47276  hoidmvlelem1  47279  hoidmvlelem2  47280  volico2  47325  2elfz2melfz  48022  m1mod0mod1  48064  m1modmmod  48068  pgnbgreunbgrlem2lem1  48846  pgnbgreunbgrlem2lem2  48847  eenglngeehlnmlem2  49485  rrx2linest  49489  line2x  49501  itscnhlc0yqe  49506  itsclc0yqsollem1  49509