Theorem subid1d 11468

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  (class class class)co 7352  ℂcc 11011  0cc0 11013   − cmin 11351

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pow 5305  ax-pr 5372  ax-un 7674  ax-resscn 11070  ax-1cn 11071  ax-icn 11072  ax-addcl 11073  ax-addrcl 11074  ax-mulcl 11075  ax-mulrcl 11076  ax-mulcom 11077  ax-addass 11078  ax-mulass 11079  ax-distr 11080  ax-i2m1 11081  ax-1ne0 11082  ax-1rid 11083  ax-rnegex 11084  ax-rrecex 11085  ax-cnre 11086  ax-pre-lttri 11087  ax-pre-lttrn 11088  ax-pre-ltadd 11089

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-nel 3034  df-ral 3049  df-rex 3058  df-reu 3348  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-mpt 5175  df-id 5514  df-po 5527  df-so 5528  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  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 7309  df-ov 7355  df-oprab 7356  df-mpo 7357  df-er 8628  df-en 8876  df-dom 8877  df-sdom 8878  df-pnf 11155  df-mnf 11156  df-ltxr 11158  df-sub 11353

This theorem is referenced by:  suble0  11638  lesub0  11641  ltm1  11970  nn0sub  12438  max0sub  13097  modid  13802  modeqmodmin  13850  muldivbinom2  14172  bcn0  14219  bcnn  14221  hashfzo0  14339  hashfz0  14341  ccatlid  14496  pfxmpt  14588  pfxfv  14592  swrdpfx  14616  pfxpfx  14617  cshwsublen  14705  remul2  15039  clim0c  15416  rlimrecl  15489  o1rlimmul  15528  rlimno1  15563  incexclem  15745  supcvg  15765  pwdif  15777  geolim  15779  fallfacval3  15921  binomfallfaclem2  15949  bpolydiflem  15963  bpoly3  15967  addmodlteqALT  16238  dvdsmod  16242  ndvdssub  16322  nn0seqcvgd  16483  phiprmpw  16689  pczpre  16761  pcaddlem  16802  pcmpt2  16807  prmreclem4  16833  4sqlem9  16860  4sqlem11  16869  ramcl  16943  oddvdsnn0  19458  odf1o2  19487  srgbinomlem4  20149  zndvds0  21489  freshmansdream  21513  psrlidm  21900  psdmul  22082  coe1sclmul  22197  coe1sclmul2  22199  cply1mul  22212  recld2  24731  i1fadd  25624  mbfi1fseqlem6  25649  itgposval  25725  dveflem  25911  dv11cn  25934  lhop1lem  25946  coemulc  26188  plydivlem3  26231  plyrem  26241  vieta1lem2  26247  aareccl  26262  aalioulem3  26270  aaliou2b  26277  dvntaylp  26307  taylthlem1  26309  psercn  26364  pserdvlem2  26366  abelthlem2  26370  abelthlem3  26371  abelthlem5  26373  abelthlem7  26376  sinmpi  26424  cosppi  26427  sinhalfpim  26430  sincosq2sgn  26436  logcnlem3  26581  logcnlem4  26582  advlog  26591  efopn  26595  logtayl  26597  pythag  26755  chordthmlem5  26774  atanlogsublem  26853  rlimcnp  26903  efrlim  26907  efrlimOLD  26908  rlimcxp  26912  cxploglim2  26917  emcllem5  26938  zetacvg  26953  lgamgulmlem2  26968  lgamcvg2  26993  0sgmppw  27137  ppiub  27143  chtublem  27150  logfacrlim  27163  logexprlim  27164  chtppilimlem2  27413  rplogsumlem2  27424  dchrisumlem3  27430  dchrvmasumiflem1  27440  dchrisum0lem2  27457  selberg2lem  27489  logdivbnd  27495  pntrsumo1  27504  pntrlog2bndlem4  27519  pntpbnd1  27525  axlowdimlem17  28938  crctcshlem4  29800  clwlkclwwlklem2a1  29974  clwlkclwwlklem2a  29980  clwlkclwwlklem3  29983  clwlkclwwlk  29984  ipidsq  30692  nmcfnexi  32033  sgnsub  32825  esplyind  33613  constrrtcc  33769  nn0constr  33795  constraddcl  33796  constrnegcl  33797  constrdircl  33799  constrremulcl  33801  constrrecl  33803  constrimcl  33804  constrmulcl  33805  constrreinvcl  33806  constrinvcl  33807  constrresqrtcl  33811  constrabscl  33812  cos9thpiminplylem1  33816  cos9thpinconstrlem1  33823  knoppndvlem10  36586  poimirlem19  37699  poimirlem20  37700  ftc1anc  37761  cntotbnd  37856  aks4d1p1p2  42183  aks4d1p1p7  42187  posbezout  42213  bcled  42291  irrapxlem3  42941  irrapxlem4  42942  pell14qrgt0  42976  pell1qrgaplem  42990  acongeq  43100  jm2.18  43105  hashnzfz  44437  hashnzfz2  44438  hashnzfzclim  44439  bccn1  44461  binomcxplemnotnn0  44473  dstregt0  45407  absimlere  45601  ellimcabssub0  45741  0ellimcdiv  45771  clim0cf  45776  fprodsubrecnncnvlem  46029  ioodvbdlimc2lem  46056  dvnxpaek  46064  dvnmul  46065  itgsbtaddcnst  46104  stoweidlem7  46129  stoweidlem11  46133  stoweidlem26  46148  dirkertrigeqlem2  46221  fourierdlem57  46285  fourierdlem60  46288  fourierdlem61  46289  fourierdlem68  46296  fourierdlem104  46332  fourierdlem107  46335  fourierdlem109  46337  etransclem4  46360  etransclem23  46379  etransclem27  46383  etransclem31  46387  etransclem35  46391  sigarexp  46981  sigaradd  46988  m1modmmod  47482  dignn0flhalflem1  48740  ehl2eudisval0  48850  2sphere0  48875  line2  48877  line2x  48879  itschlc0yqe  48885  itschlc0xyqsol1  48891  itschlc0xyqsol  48892