Theorem subidd 11635

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108  (class class class)co 7448  ℂcc 11182  0cc0 11184   − cmin 11520

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-resscn 11241  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-mulcom 11248  ax-addass 11249  ax-mulass 11250  ax-distr 11251  ax-i2m1 11252  ax-1ne0 11253  ax-1rid 11254  ax-rnegex 11255  ax-rrecex 11256  ax-cnre 11257  ax-pre-lttri 11258  ax-pre-lttrn 11259  ax-pre-ltadd 11260

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-po 5607  df-so 5608  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-riota 7404  df-ov 7451  df-oprab 7452  df-mpo 7453  df-er 8763  df-en 9004  df-dom 9005  df-sdom 9006  df-pnf 11326  df-mnf 11327  df-ltxr 11329  df-sub 11522

This theorem is referenced by:  mulsubaddmulsub  11754  leaddle0  11805  cru  12285  iccf1o  13556  fzocatel  13780  zmod10  13938  hashfzo  14478  hashfzp1  14480  ccatval21sw  14633  ccats1val2  14675  swrd00  14692  ccatpfx  14749  swrdccat3blem  14787  revccat  14814  repswswrd  14832  climconst  15589  rlimconst  15590  telfsumo  15850  fsumparts  15854  incexc  15885  pwdif  15916  cvgrat  15931  binomfallfaclem2  16088  fallfacfac  16093  bpolysum  16101  divalglem5  16445  nn0seqcvgd  16617  pcmpt2  16940  4sqlem15  17006  efgtlen  19768  srgbinomlem3  20255  fermltlchr  21567  freshmansdream  21616  cayhamlem1  22893  vitalilem1  25662  dvcnp2  25975  dvcnp2OLD  25976  dvferm1lem  26042  c1lip1  26056  dv11cn  26060  ftc1lem5  26101  ftc2  26105  plyeq0lem  26269  dgrcolem2  26334  plydivlem4  26356  qaa  26383  aalioulem3  26394  aaliou3lem2  26403  tayl0  26421  dvntaylp  26431  taylthlem1  26433  taylthlem2  26434  taylthlem2OLD  26435  abelthlem9  26502  isosctrlem1  26879  birthdaylem2  27013  rlimcnp  27026  lgam1  27125  basellem2  27143  basellem5  27146  chpub  27282  dchrsum2  27330  sumdchr2  27332  2sqmod  27498  rplogsumlem2  27547  dchrisumlem1  27551  pntlemf  27667  colinearalglem4  28942  crctcsh  29857  eucrct2eupth  30277  ipidsq  30742  dip0r  30749  riesz3i  32094  riesz4i  32095  hmopidmpji  32184  pjclem4  32231  pj3si  32239  cycpmco2lem2  33120  cycpmco2lem4  33122  cycpmco2lem6  33124  znfermltl  33359  ccfldextdgrr  33682  constrrtcc  33726  signsply0  34528  itgexpif  34583  dnizeq0  36441  unbdqndv2lem2  36476  poimir  37613  itg2addnclem3  37633  ftc1cnnc  37652  ftc2nc  37662  areacirc  37673  posbezout  42057  aks6d1c5lem1  42093  aks6d1c5lem2  42095  sticksstones10  42112  sticksstones12a  42114  bcle2d  42136  metakunt24  42185  lsubswap23d  42268  fltnltalem  42617  3cubeslem2  42641  congid  42928  congabseq  42931  jm2.18  42945  dgrsub2  43092  areaquad  43177  ofsubid  44293  isosctrlem1ALT  44905  supxrgelem  45252  constlimc  45545  ioodvbdlimc1lem1  45852  dvnxpaek  45863  dvnmul  45864  voliooico  45913  voliccico  45920  stoweidlem13  45934  stoweidlem23  45944  stoweidlem26  45947  stirlinglem5  45999  dirkertrigeqlem2  46020  fourierdlem4  46032  fourierdlem42  46070  fourierdlem60  46087  fourierdlem61  46088  fourierdlem74  46101  fourierdlem75  46102  fourierdlem89  46116  fourierdlem90  46117  fourierdlem91  46118  fourierdlem103  46130  fourierdlem104  46131  fourierdlem107  46134  sqwvfoura  46149  etransclem24  46179  etransclem25  46180  hoidmv1lelem1  46512  hoidmv1lelem2  46513  hoidmvlelem1  46516  hoidmvlelem2  46517  volico2  46562  2elfz2melfz  47233  m1mod0mod1  47243  m1modmmod  48255  eenglngeehlnmlem2  48472  rrx2linest  48476  line2x  48488  itscnhlc0yqe  48493  itsclc0yqsollem1  48496