Theorem subid1d 11482

Description: Identity law for subtraction. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
negidd.1	⊢ (𝜑 → 𝐴 ∈ ℂ)

Assertion

Ref	Expression
subid1d	⊢ (𝜑 → (𝐴 − 0) = 𝐴)

Proof of Theorem subid1d

Step	Hyp	Ref	Expression
1		negidd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		subid1 11402	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 − 0) = 𝐴)
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴 − 0) = 𝐴)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  (class class class)co 7353  ℂcc 11026  0cc0 11028   − cmin 11365

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7675  ax-resscn 11085  ax-1cn 11086  ax-icn 11087  ax-addcl 11088  ax-addrcl 11089  ax-mulcl 11090  ax-mulrcl 11091  ax-mulcom 11092  ax-addass 11093  ax-mulass 11094  ax-distr 11095  ax-i2m1 11096  ax-1ne0 11097  ax-1rid 11098  ax-rnegex 11099  ax-rrecex 11100  ax-cnre 11101  ax-pre-lttri 11102  ax-pre-lttrn 11103  ax-pre-ltadd 11104

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3346  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5518  df-po 5531  df-so 5532  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-riota 7310  df-ov 7356  df-oprab 7357  df-mpo 7358  df-er 8632  df-en 8880  df-dom 8881  df-sdom 8882  df-pnf 11170  df-mnf 11171  df-ltxr 11173  df-sub 11367

This theorem is referenced by:  suble0  11652  lesub0  11655  ltm1  11984  nn0sub  12452  max0sub  13116  modid  13818  modeqmodmin  13866  muldivbinom2  14188  bcn0  14235  bcnn  14237  hashfzo0  14355  hashfz0  14357  ccatlid  14511  pfxmpt  14603  pfxfv  14607  swrdpfx  14631  pfxpfx  14632  cshwsublen  14720  remul2  15055  clim0c  15432  rlimrecl  15505  o1rlimmul  15544  rlimno1  15579  incexclem  15761  supcvg  15781  pwdif  15793  geolim  15795  fallfacval3  15937  binomfallfaclem2  15965  bpolydiflem  15979  bpoly3  15983  addmodlteqALT  16254  dvdsmod  16258  ndvdssub  16338  nn0seqcvgd  16499  phiprmpw  16705  pczpre  16777  pcaddlem  16818  pcmpt2  16823  prmreclem4  16849  4sqlem9  16876  4sqlem11  16885  ramcl  16959  oddvdsnn0  19441  odf1o2  19470  srgbinomlem4  20132  zndvds0  21475  freshmansdream  21499  psrlidm  21887  psdmul  22069  coe1sclmul  22184  coe1sclmul2  22186  cply1mul  22199  recld2  24719  i1fadd  25612  mbfi1fseqlem6  25637  itgposval  25713  dveflem  25899  dv11cn  25922  lhop1lem  25934  coemulc  26176  plydivlem3  26219  plyrem  26229  vieta1lem2  26235  aareccl  26250  aalioulem3  26258  aaliou2b  26265  dvntaylp  26295  taylthlem1  26297  psercn  26352  pserdvlem2  26354  abelthlem2  26358  abelthlem3  26359  abelthlem5  26361  abelthlem7  26364  sinmpi  26412  cosppi  26415  sinhalfpim  26418  sincosq2sgn  26424  logcnlem3  26569  logcnlem4  26570  advlog  26579  efopn  26583  logtayl  26585  pythag  26743  chordthmlem5  26762  atanlogsublem  26841  rlimcnp  26891  efrlim  26895  efrlimOLD  26896  rlimcxp  26900  cxploglim2  26905  emcllem5  26926  zetacvg  26941  lgamgulmlem2  26956  lgamcvg2  26981  0sgmppw  27125  ppiub  27131  chtublem  27138  logfacrlim  27151  logexprlim  27152  chtppilimlem2  27401  rplogsumlem2  27412  dchrisumlem3  27418  dchrvmasumiflem1  27428  dchrisum0lem2  27445  selberg2lem  27477  logdivbnd  27483  pntrsumo1  27492  pntrlog2bndlem4  27507  pntpbnd1  27513  axlowdimlem17  28921  crctcshlem4  29783  clwlkclwwlklem2a1  29954  clwlkclwwlklem2a  29960  clwlkclwwlklem3  29963  clwlkclwwlk  29964  ipidsq  30672  nmcfnexi  32013  sgnsub  32795  constrrtcc  33701  nn0constr  33727  constraddcl  33728  constrnegcl  33729  constrdircl  33731  constrremulcl  33733  constrrecl  33735  constrimcl  33736  constrmulcl  33737  constrreinvcl  33738  constrinvcl  33739  constrresqrtcl  33743  constrabscl  33744  cos9thpiminplylem1  33748  cos9thpinconstrlem1  33755  knoppndvlem10  36494  poimirlem19  37618  poimirlem20  37619  ftc1anc  37680  cntotbnd  37775  aks4d1p1p2  42043  aks4d1p1p7  42047  posbezout  42073  bcled  42151  irrapxlem3  42797  irrapxlem4  42798  pell14qrgt0  42832  pell1qrgaplem  42846  acongeq  42956  jm2.18  42961  hashnzfz  44293  hashnzfz2  44294  hashnzfzclim  44295  bccn1  44317  binomcxplemnotnn0  44329  dstregt0  45264  absimlere  45459  ellimcabssub0  45599  0ellimcdiv  45631  clim0cf  45636  fprodsubrecnncnvlem  45889  ioodvbdlimc2lem  45916  dvnxpaek  45924  dvnmul  45925  itgsbtaddcnst  45964  stoweidlem7  45989  stoweidlem11  45993  stoweidlem26  46008  dirkertrigeqlem2  46081  fourierdlem57  46145  fourierdlem60  46148  fourierdlem61  46149  fourierdlem68  46156  fourierdlem104  46192  fourierdlem107  46195  fourierdlem109  46197  etransclem4  46220  etransclem23  46239  etransclem27  46243  etransclem31  46247  etransclem35  46251  sigarexp  46841  sigaradd  46848  m1modmmod  47343  dignn0flhalflem1  48601  ehl2eudisval0  48711  2sphere0  48736  line2  48738  line2x  48740  itschlc0yqe  48746  itschlc0xyqsol1  48752  itschlc0xyqsol  48753