Theorem subid1d 11559

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

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143  (class class class)co 7412  ℂcc 11099  0cc0 11101   − cmin 11442

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pow 5338  ax-pr 5406  ax-un 7734  ax-resscn 11158  ax-1cn 11159  ax-icn 11160  ax-addcl 11161  ax-addrcl 11162  ax-mulcl 11163  ax-mulrcl 11164  ax-mulcom 11165  ax-addass 11166  ax-mulass 11167  ax-distr 11168  ax-i2m1 11169  ax-1ne0 11170  ax-1rid 11171  ax-rnegex 11172  ax-rrecex 11173  ax-cnre 11174  ax-pre-lttri 11175  ax-pre-lttrn 11176  ax-pre-ltadd 11177

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3746  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5558  df-po 5571  df-so 5572  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7369  df-ov 7415  df-oprab 7416  df-mpo 7417  df-er 8695  df-en 8945  df-dom 8946  df-sdom 8947  df-pnf 11246  df-mnf 11247  df-ltxr 11249  df-sub 11444

This theorem is referenced by:  suble0  11729  lesub0  11732  ltm1  12058  nn0sub  12555  max0sub  13223  modid  13931  modeqmodmin  13979  muldivbinom2  14301  bcn0  14348  bcnn  14350  hashfzo0  14469  hashfz0  14471  ccatlid  14626  pfxmpt  14718  pfxfv  14722  swrdpfx  14746  pfxpfx  14747  cshwsublen  14835  sgnsub  15145  remul2  15183  clim0c  15560  rlimrecl  15633  o1rlimmul  15672  rlimno1  15707  incexclem  15892  supcvg  15912  pwdif  15924  geolim  15926  fallfacval3  16068  binomfallfaclem2  16095  bpolydiflem  16109  bpoly3  16113  addmodlteqALT  16384  dvdsmod  16388  ndvdssub  16468  nn0seqcvgd  16629  phiprmpw  16836  pczpre  16908  pcaddlem  16949  pcmpt2  16954  prmreclem4  16980  4sqlem9  17007  4sqlem11  17016  ramcl  17090  oddvdsnn0  19615  odf1o2  19644  srgbinomlem4  20312  zndvds0  21681  freshmansdream  21705  psrlidm  22092  psdmul  22310  coe1sclmul  22424  coe1sclmul2  22426  cply1mul  22437  recld2  24953  i1fadd  25835  mbfi1fseqlem6  25860  itgposval  25936  dveflem  26119  dv11cn  26141  lhop1lem  26153  coemulc  26393  plydivlem3  26437  plyrem  26447  vieta1lem2  26453  aareccl  26468  aalioulem3  26476  aaliou2b  26483  dvntaylp  26512  taylthlem1  26514  psercn  26567  pserdvlem2  26569  abelthlem2  26573  abelthlem3  26574  abelthlem5  26576  abelthlem7  26579  sinmpi  26630  cosppi  26633  sinhalfpim  26636  sincosq2sgn  26642  logcnlem3  26787  logcnlem4  26788  advlog  26797  efopn  26801  logtayl  26803  pythag  26960  chordthmlem5  26979  atanlogsublem  27058  rlimcnp  27108  efrlim  27112  rlimcxp  27116  cxploglim2  27121  emcllem5  27142  zetacvg  27157  lgamgulmlem2  27172  lgamcvg2  27197  0sgmppw  27340  ppiub  27346  chtublem  27353  logfacrlim  27366  logexprlim  27367  chtppilimlem2  27616  rplogsumlem2  27627  dchrisumlem3  27633  dchrvmasumiflem1  27643  dchrisum0lem2  27660  selberg2lem  27692  logdivbnd  27698  pntrsumo1  27707  pntrlog2bndlem4  27722  pntpbnd1  27728  axlowdimlem17  29286  crctcshlem4  30147  clwlkclwwlklem2a1  30321  clwlkclwwlklem2a  30327  clwlkclwwlklem3  30330  clwlkclwwlk  30331  ipidsq  31040  nmcfnexi  32381  esplyind  33943  vietalem  33947  constrrtcc  34103  nn0constr  34129  constraddcl  34130  constrnegcl  34131  constrdircl  34133  constrremulcl  34135  constrrecl  34137  constrimcl  34138  constrmulcl  34139  constrreinvcl  34140  constrinvcl  34141  constrresqrtcl  34145  constrabscl  34146  cos9thpiminplylem1  34150  cos9thpinconstrlem1  34157  knoppndvlem10  37088  poimirlem19  38268  poimirlem20  38269  ftc1anc  38330  cntotbnd  38425  aks4d1p1p2  42815  aks4d1p1p7  42819  posbezout  42845  bcled  42923  irrapxlem3  43531  irrapxlem4  43532  pell14qrgt0  43566  pell1qrgaplem  43580  acongeq  43690  jm2.18  43695  hashnzfz  45010  hashnzfz2  45011  hashnzfzclim  45012  bccn1  45034  binomcxplemnotnn0  45046  dstregt0  45981  absimlere  46173  ellimcabssub0  46313  0ellimcdiv  46343  clim0cf  46348  fprodsubrecnncnvlem  46601  ioodvbdlimc2lem  46628  dvnxpaek  46636  dvnmul  46637  itgsbtaddcnst  46676  stoweidlem7  46701  stoweidlem11  46705  stoweidlem26  46720  dirkertrigeqlem2  46793  fourierdlem57  46857  fourierdlem60  46860  fourierdlem61  46861  fourierdlem68  46868  fourierdlem104  46904  fourierdlem107  46907  fourierdlem109  46909  etransclem4  46932  etransclem23  46951  etransclem27  46955  etransclem31  46959  etransclem35  46963  sigarexp  47553  sigaradd  47560  m1modmmod  48078  dignn0flhalflem1  49372  ehl2eudisval0  49482  2sphere0  49507  line2  49509  line2x  49511  itschlc0yqe  49517  itschlc0xyqsol1  49523  itschlc0xyqsol  49524