Theorem subid1d 11636

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108  (class class class)co 7448  ℂcc 11182  0cc0 11184   − cmin 11520

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-resscn 11241  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-mulcom 11248  ax-addass 11249  ax-mulass 11250  ax-distr 11251  ax-i2m1 11252  ax-1ne0 11253  ax-1rid 11254  ax-rnegex 11255  ax-rrecex 11256  ax-cnre 11257  ax-pre-lttri 11258  ax-pre-lttrn 11259  ax-pre-ltadd 11260

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-po 5607  df-so 5608  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-riota 7404  df-ov 7451  df-oprab 7452  df-mpo 7453  df-er 8763  df-en 9004  df-dom 9005  df-sdom 9006  df-pnf 11326  df-mnf 11327  df-ltxr 11329  df-sub 11522

This theorem is referenced by:  suble0  11804  lesub0  11807  ltm1  12136  nn0sub  12603  max0sub  13258  modid  13947  modeqmodmin  13992  muldivbinom2  14312  bcn0  14359  bcnn  14361  hashfzo0  14479  hashfz0  14481  ccatlid  14634  pfxmpt  14726  pfxfv  14730  swrdpfx  14755  pfxpfx  14756  cshwsublen  14844  remul2  15179  clim0c  15553  rlimrecl  15626  o1rlimmul  15665  rlimno1  15702  incexclem  15884  supcvg  15904  pwdif  15916  geolim  15918  fallfacval3  16060  binomfallfaclem2  16088  bpolydiflem  16102  bpoly3  16106  addmodlteqALT  16373  dvdsmod  16377  ndvdssub  16457  nn0seqcvgd  16617  phiprmpw  16823  pczpre  16894  pcaddlem  16935  pcmpt2  16940  prmreclem4  16966  4sqlem9  16993  4sqlem11  17002  ramcl  17076  oddvdsnn0  19586  odf1o2  19615  srgbinomlem4  20256  zndvds0  21592  freshmansdream  21616  psrlidm  22005  psdmul  22193  coe1sclmul  22306  coe1sclmul2  22308  cply1mul  22321  recld2  24855  i1fadd  25749  mbfi1fseqlem6  25775  itgposval  25851  dveflem  26037  dv11cn  26060  lhop1lem  26072  coemulc  26314  plydivlem3  26355  plyrem  26365  vieta1lem2  26371  aareccl  26386  aalioulem3  26394  aaliou2b  26401  dvntaylp  26431  taylthlem1  26433  psercn  26488  pserdvlem2  26490  abelthlem2  26494  abelthlem3  26495  abelthlem5  26497  abelthlem7  26500  sinmpi  26547  cosppi  26550  sinhalfpim  26553  sincosq2sgn  26559  logcnlem3  26704  logcnlem4  26705  advlog  26714  efopn  26718  logtayl  26720  pythag  26878  chordthmlem5  26897  atanlogsublem  26976  rlimcnp  27026  efrlim  27030  efrlimOLD  27031  rlimcxp  27035  cxploglim2  27040  emcllem5  27061  zetacvg  27076  lgamgulmlem2  27091  lgamcvg2  27116  0sgmppw  27260  ppiub  27266  chtublem  27273  logfacrlim  27286  logexprlim  27287  chtppilimlem2  27536  rplogsumlem2  27547  dchrisumlem3  27553  dchrvmasumiflem1  27563  dchrisum0lem2  27580  selberg2lem  27612  logdivbnd  27618  pntrsumo1  27627  pntrlog2bndlem4  27642  pntpbnd1  27648  axlowdimlem17  28991  crctcshlem4  29853  clwlkclwwlklem2a1  30024  clwlkclwwlklem2a  30030  clwlkclwwlklem3  30033  clwlkclwwlk  30034  ipidsq  30742  nmcfnexi  32083  constrrtcc  33726  sgnsub  34509  knoppndvlem10  36487  poimirlem19  37599  poimirlem20  37600  ftc1anc  37661  cntotbnd  37756  aks4d1p1p2  42027  aks4d1p1p7  42031  posbezout  42057  bcled  42135  irrapxlem3  42780  irrapxlem4  42781  pell14qrgt0  42815  pell1qrgaplem  42829  acongeq  42940  jm2.18  42945  hashnzfz  44289  hashnzfz2  44290  hashnzfzclim  44291  bccn1  44313  binomcxplemnotnn0  44325  dstregt0  45196  absimlere  45395  ellimcabssub0  45538  0ellimcdiv  45570  clim0cf  45575  fprodsubrecnncnvlem  45828  ioodvbdlimc2lem  45855  dvnxpaek  45863  dvnmul  45864  itgsbtaddcnst  45903  stoweidlem7  45928  stoweidlem11  45932  stoweidlem26  45947  dirkertrigeqlem2  46020  fourierdlem57  46084  fourierdlem60  46087  fourierdlem61  46088  fourierdlem68  46095  fourierdlem104  46131  fourierdlem107  46134  fourierdlem109  46136  etransclem4  46159  etransclem23  46178  etransclem27  46182  etransclem31  46186  etransclem35  46190  sigarexp  46780  sigaradd  46787  m1modmmod  48255  dignn0flhalflem1  48349  ehl2eudisval0  48459  2sphere0  48484  line2  48486  line2x  48488  itschlc0yqe  48494  itschlc0xyqsol1  48500  itschlc0xyqsol  48501