Theorem subid1d 11685

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147  (class class class)co 7443  ℂcc 11225  0cc0 11227   − cmin 11568

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7775  ax-resscn 11284  ax-1cn 11285  ax-icn 11286  ax-addcl 11287  ax-addrcl 11288  ax-mulcl 11289  ax-mulrcl 11290  ax-mulcom 11291  ax-addass 11292  ax-mulass 11293  ax-distr 11294  ax-i2m1 11295  ax-1ne0 11296  ax-1rid 11297  ax-rnegex 11298  ax-rrecex 11299  ax-cnre 11300  ax-pre-lttri 11301  ax-pre-lttrn 11302  ax-pre-ltadd 11303

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-po 5563  df-so 5564  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6512  df-fun 6560  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-fv 6566  df-riota 7400  df-ov 7446  df-oprab 7447  df-mpo 7448  df-er 8745  df-en 9002  df-dom 9003  df-sdom 9004  df-pnf 11372  df-mnf 11373  df-ltxr 11375  df-sub 11570

This theorem is used by:  suble0  11857  lesub0  11860  ltm1  12186  nn0sub  12683  max0sub  13353  modid  14063  modeqmodmin  14111  muldivbinom2  14434  bcn0  14481  bcnn  14483  hashfzo0  14602  hashfz0  14604  ccatlid  14759  pfxmpt  14856  pfxfv  14860  swrdpfx  14884  pfxpfx  14885  cshwsublen  14975  sgnsub  15288  remul2  15326  clim0c  15703  rlimrecl  15776  o1rlimmul  15815  rlimno1  15850  incexclem  16034  supcvg  16054  pwdif  16066  geolim  16068  fallfacval3  16208  binomfallfaclem2  16235  bpolydiflem  16249  bpoly3  16253  addmodlteqALT  16524  dvdsmod  16528  ndvdssub  16608  nn0seqcvgd  16774  phiprmpw  16982  pczpre  17054  pcaddlem  17095  pcmpt2  17100  prmreclem4  17126  4sqlem9  17153  4sqlem11  17162  ramcl  17236  oddvdsnn0  19788  odf1o2  19817  srgbinomlem4  20485  zndvds0  21886  freshmansdream  21910  psrlidm  22299  psdmul  22517  coe1sclmul  22631  coe1sclmul2  22633  cply1mul  22644  recld2  25164  i1fadd  26046  mbfi1fseqlem6  26071  itgposval  26146  dveflem  26329  dv11cn  26351  lhop1lem  26363  coemulc  26604  plydivlem3  26646  plyrem  26656  vieta1lem2  26664  aareccl  26683  aalioulem3  26691  aaliou2b  26698  dvntaylp  26728  taylthlem1  26730  psercn  26783  pserdvlem2  26785  abelthlem2  26789  abelthlem3  26790  abelthlem5  26792  abelthlem7  26795  sinmpi  26846  cosppi  26849  sinhalfpim  26852  sincosq2sgn  26858  logcnlem3  27002  logcnlem4  27003  advlog  27012  efopn  27016  logtayl  27018  pythag  27175  chordthmlem5  27194  atanlogsublem  27273  rlimcnp  27323  efrlim  27327  rlimcxp  27331  cxploglim2  27336  emcllem5  27357  zetacvg  27372  lgamgulmlem2  27387  lgamcvg2  27412  0sgmppw  27555  ppiub  27561  chtublem  27568  logfacrlim  27581  logexprlim  27582  chtppilimlem2  27831  rplogsumlem2  27842  dchrisumlem3  27848  dchrvmasumiflem1  27858  dchrisum0lem2  27875  selberg2lem  27907  logdivbnd  27913  pntrsumo1  27922  pntrlog2bndlem4  27937  pntpbnd1  27943  axlowdimlem17  29566  crctcshlem4  30439  clwlkclwwlklem2a1  30613  clwlkclwwlklem2a  30619  clwlkclwwlklem3  30622  clwlkclwwlk  30623  ipidsq  31342  nmcfnexi  32683  esplyind  34277  vietalem  34281  constrrtcc  34437  nn0constr  34463  constraddcl  34464  constrnegcl  34465  constrdircl  34467  constrremulcl  34469  constrrecl  34471  constrimcl  34472  constrmulcl  34473  constrreinvcl  34474  constrinvcl  34475  constrresqrtcl  34479  constrabscl  34480  cos9thpiminplylem1  34484  cos9thpinconstrlem1  34491  knoppndvlem10  37565  poimirlem19  38749  poimirlem20  38750  ftc1anc  38811  cntotbnd  38922  aks4d1p1p2  43312  aks4d1p1p7  43316  posbezout  43342  bcled  43420  irrapxlem3  44024  irrapxlem4  44025  pell14qrgt0  44059  pell1qrgaplem  44073  acongeq  44183  jm2.18  44188  hashnzfz  45496  hashnzfz2  45497  hashnzfzclim  45498  bccn1  45520  binomcxplemnotnn0  45532  dstregt0  46503  absimlere  46694  ellimcabssub0  46834  0ellimcdiv  46864  clim0cf  46869  fprodsubrecnncnvlem  47122  ioodvbdlimc2lem  47149  dvnxpaek  47157  dvnmul  47158  itgsbtaddcnst  47197  stoweidlem7  47222  stoweidlem11  47226  stoweidlem26  47241  dirkertrigeqlem2  47314  fourierdlem57  47378  fourierdlem60  47381  fourierdlem61  47382  fourierdlem68  47389  fourierdlem104  47425  fourierdlem107  47428  fourierdlem109  47430  etransclem4  47453  etransclem23  47472  etransclem27  47476  etransclem31  47480  etransclem35  47484  sigarexp  48074  sigaradd  48081  m1modmmod  48639  dignn0flhalflem1  49932  ehl2eudisval0  50043  2sphere0  50067  line2  50069  line2x  50071  itschlc0yqe  50077  itschlc0xyqsol1  50083  itschlc0xyqsol  50084