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

Theorem subid1d 10974
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 10894 . 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 10523  0cc0 10525  cmin 10858
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 2790  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-resscn 10582  ax-1cn 10583  ax-icn 10584  ax-addcl 10585  ax-addrcl 10586  ax-mulcl 10587  ax-mulrcl 10588  ax-mulcom 10589  ax-addass 10590  ax-mulass 10591  ax-distr 10592  ax-i2m1 10593  ax-1ne0 10594  ax-1rid 10595  ax-rnegex 10596  ax-rrecex 10597  ax-cnre 10598  ax-pre-lttri 10599  ax-pre-lttrn 10600  ax-pre-ltadd 10601
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 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-nel 3121  df-ral 3140  df-rex 3141  df-reu 3142  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-po 5467  df-so 5468  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-er 8278  df-en 8498  df-dom 8499  df-sdom 8500  df-pnf 10665  df-mnf 10666  df-ltxr 10668  df-sub 10860
This theorem is referenced by:  suble0  11142  lesub0  11145  ltm1  11470  nn0sub  11935  max0sub  12577  modid  13252  modeqmodmin  13297  muldivbinom2  13611  bcn0  13658  bcnn  13660  hashfzo0  13779  hashfz0  13781  ccatlid  13928  pfxmpt  14028  pfxfv  14032  swrdpfx  14057  pfxpfx  14058  cshwsublen  14146  remul2  14477  clim0c  14852  rlimrecl  14925  o1rlimmul  14963  rlimno1  14998  incexclem  15179  supcvg  15199  pwdif  15211  geolim  15214  fallfacval3  15354  binomfallfaclem2  15382  bpolydiflem  15396  bpoly3  15400  addmodlteqALT  15663  dvdsmod  15666  ndvdssub  15748  nn0seqcvgd  15902  phiprmpw  16101  pczpre  16172  pcaddlem  16212  pcmpt2  16217  prmreclem4  16243  4sqlem9  16270  4sqlem11  16279  ramcl  16353  oddvdsnn0  18601  odf1o2  18627  srgbinomlem4  19222  psrlidm  20111  coe1sclmul  20378  coe1sclmul2  20380  cply1mul  20390  zndvds0  20625  recld2  23349  i1fadd  24223  mbfi1fseqlem6  24248  itgposval  24323  dveflem  24503  dv11cn  24525  lhop1lem  24537  coemulc  24772  plydivlem3  24811  plyrem  24821  vieta1lem2  24827  aareccl  24842  aalioulem3  24850  aaliou2b  24857  dvntaylp  24886  taylthlem1  24888  psercn  24941  pserdvlem2  24943  abelthlem2  24947  abelthlem3  24948  abelthlem5  24950  abelthlem7  24953  sinmpi  25000  cosppi  25003  sinhalfpim  25006  sincosq2sgn  25012  logcnlem3  25154  logcnlem4  25155  advlog  25164  efopn  25168  logtayl  25170  pythag  25322  chordthmlem5  25341  atanlogsublem  25420  rlimcnp  25470  efrlim  25474  rlimcxp  25478  cxploglim2  25483  emcllem5  25504  zetacvg  25519  lgamgulmlem2  25534  lgamcvg2  25559  0sgmppw  25701  ppiub  25707  chtublem  25714  logfacrlim  25727  logexprlim  25728  chtppilimlem2  25977  rplogsumlem2  25988  dchrisumlem3  25994  dchrvmasumiflem1  26004  dchrisum0lem2  26021  selberg2lem  26053  logdivbnd  26059  pntrsumo1  26068  pntrlog2bndlem4  26083  pntpbnd1  26089  axlowdimlem17  26671  crctcshlem4  27525  clwlkclwwlklem2a1  27697  clwlkclwwlklem2a  27703  clwlkclwwlklem3  27706  clwlkclwwlk  27707  ipidsq  28414  nmcfnexi  29755  freshmansdream  30786  sgnsub  31701  knoppndvlem10  33757  poimirlem19  34792  poimirlem20  34793  ftc1anc  34856  cntotbnd  34955  irrapxlem3  39299  irrapxlem4  39300  pell14qrgt0  39334  pell1qrgaplem  39348  acongeq  39458  jm2.18  39463  hashnzfz  40529  hashnzfz2  40530  hashnzfzclim  40531  bccn1  40553  binomcxplemnotnn0  40565  dstregt0  41423  absimlere  41632  ellimcabssub0  41774  0ellimcdiv  41806  clim0cf  41811  fprodsubrecnncnvlem  42067  ioodvbdlimc2lem  42095  dvnxpaek  42103  dvnmul  42104  itgsbtaddcnst  42143  stoweidlem7  42169  stoweidlem11  42173  stoweidlem26  42188  dirkertrigeqlem2  42261  fourierdlem57  42325  fourierdlem60  42328  fourierdlem61  42329  fourierdlem68  42336  fourierdlem104  42372  fourierdlem107  42375  fourierdlem109  42377  etransclem4  42400  etransclem23  42419  etransclem27  42423  etransclem31  42427  etransclem35  42431  sigarexp  42993  sigaradd  43000  m1modmmod  44509  dignn0flhalflem1  44603  ehl2eudisval0  44640  2sphere0  44665  line2  44667  line2x  44669  itschlc0yqe  44675  itschlc0xyqsol1  44681  itschlc0xyqsol  44682
  Copyright terms: Public domain W3C validator