Theorem subidd 11545

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

Syntax hints:   → wi 4   = wceq 1563   ∈ wcel 2145  (class class class)co 7400  ℂcc 11086  0cc0 11088   − cmin 11429

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5251  ax-nul 5261  ax-pow 5327  ax-pr 5395  ax-un 7722  ax-resscn 11145  ax-1cn 11146  ax-icn 11147  ax-addcl 11148  ax-addrcl 11149  ax-mulcl 11150  ax-mulrcl 11151  ax-mulcom 11152  ax-addass 11153  ax-mulass 11154  ax-distr 11155  ax-i2m1 11156  ax-1ne0 11157  ax-1rid 11158  ax-rnegex 11159  ax-rrecex 11160  ax-cnre 11161  ax-pre-lttri 11162  ax-pre-lttrn 11163  ax-pre-ltadd 11164

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3065  df-ral 3080  df-rex 3090  df-reu 3371  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-br 5106  df-opab 5168  df-mpt 5187  df-id 5547  df-po 5560  df-so 5561  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-fv 6533  df-riota 7357  df-ov 7403  df-oprab 7404  df-mpo 7405  df-er 8682  df-en 8932  df-dom 8933  df-sdom 8934  df-pnf 11233  df-mnf 11234  df-ltxr 11236  df-sub 11431

This theorem is referenced by:  mulsubaddmulsub  11666  leaddle0  11717  cru  12201  iccf1o  13514  elfzo0suble  13726  fzocatel  13749  zmod10  13911  hashfzo  14456  hashfzp1  14458  ccatval21sw  14613  ccats1val2  14655  swrd00  14672  ccatpfx  14728  swrdccat3blem  14766  revccat  14793  repswswrd  14811  climconst  15584  rlimconst  15585  telfsumo  15844  fsumparts  15848  incexc  15881  pwdif  15912  cvgrat  15927  binomfallfaclem2  16084  fallfacfac  16089  bpolysum  16097  divalglem5  16445  nn0seqcvgd  16618  pcmpt2  16943  4sqlem15  17009  efgtlen  19787  srgbinomlem3  20301  fermltlchr  21639  freshmansdream  21684  cayhamlem1  22984  vitalilem1  25728  dvcnp2  26040  dvferm1lem  26104  c1lip1  26117  dv11cn  26121  ftc1lem5  26160  ftc2  26164  plyeq0lem  26328  dgrcolem2  26392  plydivlem4  26418  qaa  26445  aalioulem3  26456  aaliou3lem2  26465  tayl0  26483  dvntaylp  26492  taylthlem1  26494  taylthlem2  26495  abelthlem9  26561  isosctrlem1  26941  birthdaylem2  27075  rlimcnp  27088  lgam1  27186  basellem2  27204  basellem5  27207  chpub  27342  dchrsum2  27390  sumdchr2  27392  2sqmod  27558  rplogsumlem2  27607  dchrisumlem1  27611  pntlemf  27727  colinearalglem4  29168  crctcsh  30082  eucrct2eupth  30505  ipidsq  30971  dip0r  30978  riesz3i  32323  riesz4i  32324  hmopidmpji  32413  pjclem4  32460  pj3si  32468  cycpmco2lem2  33360  cycpmco2lem4  33362  cycpmco2lem6  33364  znfermltl  33596  vietalem  33886  ccfldextdgrr  33979  constrrtcc  34042  signsply0  34855  itgexpif  34910  dnizeq0  36926  unbdqndv2lem2  36961  qdiff  37831  poimir  38164  itg2addnclem3  38184  ftc1cnnc  38203  ftc2nc  38213  areacirc  38224  posbezout  42729  aks6d1c5lem1  42765  aks6d1c5lem2  42767  sticksstones10  42784  sticksstones12a  42786  bcle2d  42808  fltnltalem  43256  3cubeslem2  43278  congid  43560  congabseq  43563  jm2.18  43577  dgrsub2  43724  areaquad  43805  ofsubid  44898  isosctrlem1ALT  45507  supxrgelem  45911  constlimc  46198  ioodvbdlimc1lem1  46503  dvnxpaek  46514  dvnmul  46515  voliooico  46564  voliccico  46571  stoweidlem13  46585  stoweidlem23  46595  stoweidlem26  46598  stirlinglem5  46650  dirkertrigeqlem2  46671  fourierdlem4  46683  fourierdlem42  46721  fourierdlem60  46738  fourierdlem61  46739  fourierdlem74  46752  fourierdlem75  46753  fourierdlem89  46767  fourierdlem90  46768  fourierdlem91  46769  fourierdlem103  46781  fourierdlem104  46782  fourierdlem107  46785  sqwvfoura  46800  etransclem24  46830  etransclem25  46831  hoidmv1lelem1  47163  hoidmv1lelem2  47164  hoidmvlelem1  47167  hoidmvlelem2  47168  volico2  47213  2elfz2melfz  47910  m1mod0mod1  47952  m1modmmod  47956  pgnbgreunbgrlem2lem1  48734  pgnbgreunbgrlem2lem2  48735  eenglngeehlnmlem2  49369  rrx2linest  49373  line2x  49385  itscnhlc0yqe  49390  itsclc0yqsollem1  49393