Theorem subidd 11629

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  (class class class)co 7408  ℂcc 11170  0cc0 11172   − cmin 11513

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7734  ax-resscn 11229  ax-1cn 11230  ax-icn 11231  ax-addcl 11232  ax-addrcl 11233  ax-mulcl 11234  ax-mulrcl 11235  ax-mulcom 11236  ax-addass 11237  ax-mulass 11238  ax-distr 11239  ax-i2m1 11240  ax-1ne0 11241  ax-1rid 11242  ax-rnegex 11243  ax-rrecex 11244  ax-cnre 11245  ax-pre-lttri 11246  ax-pre-lttrn 11247  ax-pre-ltadd 11248

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5542  df-po 5555  df-so 5556  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-iota 6483  df-fun 6529  df-fn 6530  df-f 6531  df-f1 6532  df-fo 6533  df-f1o 6534  df-fv 6535  df-riota 7365  df-ov 7411  df-oprab 7412  df-mpo 7413  df-er 8695  df-en 8952  df-dom 8953  df-sdom 8954  df-pnf 11317  df-mnf 11318  df-ltxr 11320  df-sub 11515

This theorem is used by:  mulsubaddmulsub  11750  leaddle0  11801  cru  12282  iccf1o  13597  elfzo0suble  13810  fzocatel  13833  zmod10  13996  hashfzo  14542  hashfzp1  14544  ccatval21sw  14699  ccats1val2  14743  swrd00  14760  ccatpfx  14818  swrdccat3blem  14856  revccat  14883  repswswrd  14903  climconst  15678  rlimconst  15679  telfsumo  15937  fsumparts  15941  incexc  15974  pwdif  16005  cvgrat  16020  binomfallfaclem2  16174  fallfacfac  16179  bpolysum  16187  divalglem5  16535  nn0seqcvgd  16708  pcmpt2  17033  4sqlem15  17099  efgtlen  19902  srgbinomlem3  20416  fermltlchr  21797  freshmansdream  21842  cayhamlem1  23146  vitalilem1  25891  dvcnp2  26202  dvferm1lem  26266  c1lip1  26279  dv11cn  26283  ftc1lem5  26322  ftc2  26326  plyeq0lem  26491  dgrcolem2  26555  plydivlem4  26581  qaa  26611  aalioulem3  26625  aaliou3lem2  26634  tayl0  26653  dvntaylp  26662  taylthlem1  26664  taylthlem2  26665  abelthlem9  26731  isosctrlem1  27110  birthdaylem2  27244  rlimcnp  27257  lgam1  27355  basellem2  27373  basellem5  27376  chpub  27511  dchrsum2  27559  sumdchr2  27561  2sqmod  27727  rplogsumlem2  27776  dchrisumlem1  27780  pntlemf  27896  colinearalglem4  29421  crctcsh  30347  eucrct2eupth  30780  ipidsq  31246  dip0r  31253  riesz3i  32598  riesz4i  32599  hmopidmpji  32688  pjclem4  32735  pj3si  32743  cycpmco2lem2  33622  cycpmco2lem4  33624  cycpmco2lem6  33626  znfermltl  33856  vietalem  34145  ccfldextdgrr  34238  constrrtcc  34301  signsply0  35115  itgexpif  35170  dnizeq0  37263  unbdqndv2lem2  37298  qdiff  38168  poimir  38491  itg2addnclem3  38511  ftc1cnnc  38530  ftc2nc  38540  areacirc  38551  posbezout  43070  aks6d1c5lem1  43106  aks6d1c5lem2  43108  sticksstones10  43125  sticksstones12a  43127  bcle2d  43149  fltnltalem  43612  3cubeslem2  43634  congid  43916  congabseq  43919  jm2.18  43933  dgrsub2  44080  areaquad  44161  ofsubid  45252  isosctrlem1ALT  45860  supxrgelem  46271  constlimc  46558  ioodvbdlimc1lem1  46863  dvnxpaek  46874  dvnmul  46875  voliooico  46924  voliccico  46931  stoweidlem13  46945  stoweidlem23  46955  stoweidlem26  46958  stirlinglem5  47010  dirkertrigeqlem2  47031  fourierdlem4  47043  fourierdlem42  47081  fourierdlem60  47098  fourierdlem61  47099  fourierdlem74  47112  fourierdlem75  47113  fourierdlem89  47127  fourierdlem90  47128  fourierdlem91  47129  fourierdlem103  47141  fourierdlem104  47142  fourierdlem107  47145  sqwvfoura  47160  etransclem24  47190  etransclem25  47191  hoidmv1lelem1  47523  hoidmv1lelem2  47524  hoidmvlelem1  47527  hoidmvlelem2  47528  volico2  47573  sqrtnnaa  47835  2elfz2melfz  48310  m1mod0mod1  48352  m1modmmod  48356  pgnbgreunbgrlem2lem1  49134  pgnbgreunbgrlem2lem2  49135  eenglngeehlnmlem2  49772  rrx2linest  49776  line2x  49788  itscnhlc0yqe  49793  itsclc0yqsollem1  49796