Theorem subid1d 11586

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 11506	. 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 7417  ℂcc 11126  0cc0 11128   − cmin 11469

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 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7740  ax-resscn 11185  ax-1cn 11186  ax-icn 11187  ax-addcl 11188  ax-addrcl 11189  ax-mulcl 11190  ax-mulrcl 11191  ax-mulcom 11192  ax-addass 11193  ax-mulass 11194  ax-distr 11195  ax-i2m1 11196  ax-1ne0 11197  ax-1rid 11198  ax-rnegex 11199  ax-rrecex 11200  ax-cnre 11201  ax-pre-lttri 11202  ax-pre-lttrn 11203  ax-pre-ltadd 11204

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 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-po 5567  df-so 5568  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7374  df-ov 7420  df-oprab 7421  df-mpo 7422  df-er 8700  df-en 8957  df-dom 8958  df-sdom 8959  df-pnf 11273  df-mnf 11274  df-ltxr 11276  df-sub 11471

This theorem is used by:  suble0  11756  lesub0  11759  ltm1  12085  nn0sub  12582  max0sub  13252  modid  13961  modeqmodmin  14009  muldivbinom2  14331  bcn0  14378  bcnn  14380  hashfzo0  14499  hashfz0  14501  ccatlid  14656  pfxmpt  14752  pfxfv  14756  swrdpfx  14780  pfxpfx  14781  cshwsublen  14871  sgnsub  15183  remul2  15221  clim0c  15598  rlimrecl  15671  o1rlimmul  15710  rlimno1  15745  incexclem  15929  supcvg  15949  pwdif  15961  geolim  15963  fallfacval3  16105  binomfallfaclem2  16132  bpolydiflem  16146  bpoly3  16150  addmodlteqALT  16421  dvdsmod  16425  ndvdssub  16505  nn0seqcvgd  16666  phiprmpw  16873  pczpre  16945  pcaddlem  16986  pcmpt2  16991  prmreclem4  17017  4sqlem9  17044  4sqlem11  17053  ramcl  17127  oddvdsnn0  19677  odf1o2  19706  srgbinomlem4  20374  zndvds0  21769  freshmansdream  21793  psrlidm  22182  psdmul  22400  coe1sclmul  22514  coe1sclmul2  22516  cply1mul  22527  recld2  25047  i1fadd  25929  mbfi1fseqlem6  25954  itgposval  26030  dveflem  26213  dv11cn  26235  lhop1lem  26247  coemulc  26488  plydivlem3  26532  plyrem  26542  vieta1lem2  26550  aareccl  26569  aalioulem3  26577  aaliou2b  26584  dvntaylp  26614  taylthlem1  26616  psercn  26669  pserdvlem2  26671  abelthlem2  26675  abelthlem3  26676  abelthlem5  26678  abelthlem7  26681  sinmpi  26732  cosppi  26735  sinhalfpim  26738  sincosq2sgn  26744  logcnlem3  26889  logcnlem4  26890  advlog  26899  efopn  26903  logtayl  26905  pythag  27062  chordthmlem5  27081  atanlogsublem  27160  rlimcnp  27210  efrlim  27214  rlimcxp  27218  cxploglim2  27223  emcllem5  27244  zetacvg  27259  lgamgulmlem2  27274  lgamcvg2  27299  0sgmppw  27442  ppiub  27448  chtublem  27455  logfacrlim  27468  logexprlim  27469  chtppilimlem2  27718  rplogsumlem2  27729  dchrisumlem3  27735  dchrvmasumiflem1  27745  dchrisum0lem2  27762  selberg2lem  27794  logdivbnd  27800  pntrsumo1  27809  pntrlog2bndlem4  27824  pntpbnd1  27830  axlowdimlem17  29423  crctcshlem4  30296  clwlkclwwlklem2a1  30470  clwlkclwwlklem2a  30476  clwlkclwwlklem3  30479  clwlkclwwlk  30480  ipidsq  31199  nmcfnexi  32540  esplyind  34093  vietalem  34097  constrrtcc  34253  nn0constr  34279  constraddcl  34280  constrnegcl  34281  constrdircl  34283  constrremulcl  34285  constrrecl  34287  constrimcl  34288  constrmulcl  34289  constrreinvcl  34290  constrinvcl  34291  constrresqrtcl  34295  constrabscl  34296  cos9thpiminplylem1  34300  cos9thpinconstrlem1  34307  knoppndvlem10  37226  poimirlem19  38396  poimirlem20  38397  ftc1anc  38458  cntotbnd  38554  aks4d1p1p2  42944  aks4d1p1p7  42948  posbezout  42974  bcled  43052  irrapxlem3  43673  irrapxlem4  43674  pell14qrgt0  43708  pell1qrgaplem  43722  acongeq  43832  jm2.18  43837  hashnzfz  45152  hashnzfz2  45153  hashnzfzclim  45154  bccn1  45176  binomcxplemnotnn0  45188  dstregt0  46123  absimlere  46315  ellimcabssub0  46455  0ellimcdiv  46485  clim0cf  46490  fprodsubrecnncnvlem  46743  ioodvbdlimc2lem  46770  dvnxpaek  46778  dvnmul  46779  itgsbtaddcnst  46818  stoweidlem7  46843  stoweidlem11  46847  stoweidlem26  46862  dirkertrigeqlem2  46935  fourierdlem57  46999  fourierdlem60  47002  fourierdlem61  47003  fourierdlem68  47010  fourierdlem104  47046  fourierdlem107  47049  fourierdlem109  47051  etransclem4  47074  etransclem23  47093  etransclem27  47097  etransclem31  47101  etransclem35  47105  sigarexp  47695  sigaradd  47702  m1modmmod  48260  dignn0flhalflem1  49553  ehl2eudisval0  49663  2sphere0  49688  line2  49690  line2x  49692  itschlc0yqe  49698  itschlc0xyqsol1  49704  itschlc0xyqsol  49705