MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  subid1d Structured version   Visualization version   GIF version

Theorem subid1d 10975
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
StepHypRef Expression
1 negidd.1 . 2 (𝜑𝐴 ∈ ℂ)
2 subid1 10895 . 2 (𝐴 ∈ ℂ → (𝐴 − 0) = 𝐴)
31, 2syl 17 1 (𝜑 → (𝐴 − 0) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  wcel 2105  (class class class)co 7145  cc 10524  0cc0 10526  cmin 10859
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7450  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3497  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4833  df-br 5059  df-opab 5121  df-mpt 5139  df-id 5454  df-po 5468  df-so 5469  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-er 8279  df-en 8499  df-dom 8500  df-sdom 8501  df-pnf 10666  df-mnf 10667  df-ltxr 10669  df-sub 10861
This theorem is referenced by:  suble0  11143  lesub0  11146  ltm1  11471  nn0sub  11936  max0sub  12579  modid  13254  modeqmodmin  13299  muldivbinom2  13613  bcn0  13660  bcnn  13662  hashfzo0  13781  hashfz0  13783  ccatlid  13930  pfxmpt  14030  pfxfv  14034  swrdpfx  14059  pfxpfx  14060  cshwsublen  14148  remul2  14479  clim0c  14854  rlimrecl  14927  o1rlimmul  14965  rlimno1  15000  incexclem  15181  supcvg  15201  pwdif  15213  geolim  15216  fallfacval3  15356  binomfallfaclem2  15384  bpolydiflem  15398  bpoly3  15402  addmodlteqALT  15665  dvdsmod  15668  ndvdssub  15750  nn0seqcvgd  15904  phiprmpw  16103  pczpre  16174  pcaddlem  16214  pcmpt2  16219  prmreclem4  16245  4sqlem9  16272  4sqlem11  16281  ramcl  16355  oddvdsnn0  18603  odf1o2  18629  srgbinomlem4  19224  psrlidm  20113  coe1sclmul  20380  coe1sclmul2  20382  cply1mul  20392  zndvds0  20627  recld2  23351  i1fadd  24225  mbfi1fseqlem6  24250  itgposval  24325  dveflem  24505  dv11cn  24527  lhop1lem  24539  coemulc  24774  plydivlem3  24813  plyrem  24823  vieta1lem2  24829  aareccl  24844  aalioulem3  24852  aaliou2b  24859  dvntaylp  24888  taylthlem1  24890  psercn  24943  pserdvlem2  24945  abelthlem2  24949  abelthlem3  24950  abelthlem5  24952  abelthlem7  24955  sinmpi  25002  cosppi  25005  sinhalfpim  25008  sincosq2sgn  25014  logcnlem3  25154  logcnlem4  25155  advlog  25164  efopn  25168  logtayl  25170  pythag  25322  chordthmlem5  25341  atanlogsublem  25420  rlimcnp  25471  efrlim  25475  rlimcxp  25479  cxploglim2  25484  emcllem5  25505  zetacvg  25520  lgamgulmlem2  25535  lgamcvg2  25560  0sgmppw  25702  ppiub  25708  chtublem  25715  logfacrlim  25728  logexprlim  25729  chtppilimlem2  25978  rplogsumlem2  25989  dchrisumlem3  25995  dchrvmasumiflem1  26005  dchrisum0lem2  26022  selberg2lem  26054  logdivbnd  26060  pntrsumo1  26069  pntrlog2bndlem4  26084  pntpbnd1  26090  axlowdimlem17  26672  crctcshlem4  27526  clwlkclwwlklem2a1  27698  clwlkclwwlklem2a  27704  clwlkclwwlklem3  27707  clwlkclwwlk  27708  ipidsq  28415  nmcfnexi  29756  freshmansdream  30787  sgnsub  31702  knoppndvlem10  33758  poimirlem19  34793  poimirlem20  34794  ftc1anc  34857  cntotbnd  34957  irrapxlem3  39301  irrapxlem4  39302  pell14qrgt0  39336  pell1qrgaplem  39350  acongeq  39460  jm2.18  39465  hashnzfz  40532  hashnzfz2  40533  hashnzfzclim  40534  bccn1  40556  binomcxplemnotnn0  40568  dstregt0  41427  absimlere  41636  ellimcabssub0  41778  0ellimcdiv  41810  clim0cf  41815  fprodsubrecnncnvlem  42071  ioodvbdlimc2lem  42099  dvnxpaek  42107  dvnmul  42108  itgsbtaddcnst  42147  stoweidlem7  42173  stoweidlem11  42177  stoweidlem26  42192  dirkertrigeqlem2  42265  fourierdlem57  42329  fourierdlem60  42332  fourierdlem61  42333  fourierdlem68  42340  fourierdlem104  42376  fourierdlem107  42379  fourierdlem109  42381  etransclem4  42404  etransclem23  42423  etransclem27  42427  etransclem31  42431  etransclem35  42435  sigarexp  42997  sigaradd  43004  m1modmmod  44479  dignn0flhalflem1  44573  ehl2eudisval0  44610  2sphere0  44635  line2  44637  line2x  44639  itschlc0yqe  44645  itschlc0xyqsol1  44651  itschlc0xyqsol  44652
  Copyright terms: Public domain W3C validator