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

Theorem subid1d 11502
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 11422 . 2 (𝐴 ∈ ℂ → (𝐴 − 0) = 𝐴)
31, 2syl 17 1 (𝜑 → (𝐴 − 0) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  wcel 2107  (class class class)co 7358  cc 11050  0cc0 11052  cmin 11386
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673  ax-resscn 11109  ax-1cn 11110  ax-icn 11111  ax-addcl 11112  ax-addrcl 11113  ax-mulcl 11114  ax-mulrcl 11115  ax-mulcom 11116  ax-addass 11117  ax-mulass 11118  ax-distr 11119  ax-i2m1 11120  ax-1ne0 11121  ax-1rid 11122  ax-rnegex 11123  ax-rrecex 11124  ax-cnre 11125  ax-pre-lttri 11126  ax-pre-lttrn 11127  ax-pre-ltadd 11128
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-reu 3355  df-rab 3409  df-v 3448  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-opab 5169  df-mpt 5190  df-id 5532  df-po 5546  df-so 5547  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-riota 7314  df-ov 7361  df-oprab 7362  df-mpo 7363  df-er 8649  df-en 8885  df-dom 8886  df-sdom 8887  df-pnf 11192  df-mnf 11193  df-ltxr 11195  df-sub 11388
This theorem is referenced by:  suble0  11670  lesub0  11673  ltm1  11998  nn0sub  12464  max0sub  13116  modid  13802  modeqmodmin  13847  muldivbinom2  14164  bcn0  14211  bcnn  14213  hashfzo0  14331  hashfz0  14333  ccatlid  14475  pfxmpt  14567  pfxfv  14571  swrdpfx  14596  pfxpfx  14597  cshwsublen  14685  remul2  15016  clim0c  15390  rlimrecl  15463  o1rlimmul  15502  rlimno1  15539  incexclem  15722  supcvg  15742  pwdif  15754  geolim  15756  fallfacval3  15896  binomfallfaclem2  15924  bpolydiflem  15938  bpoly3  15942  addmodlteqALT  16208  dvdsmod  16212  ndvdssub  16292  nn0seqcvgd  16447  phiprmpw  16649  pczpre  16720  pcaddlem  16761  pcmpt2  16766  prmreclem4  16792  4sqlem9  16819  4sqlem11  16828  ramcl  16902  oddvdsnn0  19327  odf1o2  19356  srgbinomlem4  19961  zndvds0  20960  psrlidm  21375  coe1sclmul  21656  coe1sclmul2  21658  cply1mul  21668  recld2  24180  i1fadd  25062  mbfi1fseqlem6  25088  itgposval  25163  dveflem  25346  dv11cn  25368  lhop1lem  25380  coemulc  25619  plydivlem3  25658  plyrem  25668  vieta1lem2  25674  aareccl  25689  aalioulem3  25697  aaliou2b  25704  dvntaylp  25733  taylthlem1  25735  psercn  25788  pserdvlem2  25790  abelthlem2  25794  abelthlem3  25795  abelthlem5  25797  abelthlem7  25800  sinmpi  25847  cosppi  25850  sinhalfpim  25853  sincosq2sgn  25859  logcnlem3  26002  logcnlem4  26003  advlog  26012  efopn  26016  logtayl  26018  pythag  26170  chordthmlem5  26189  atanlogsublem  26268  rlimcnp  26318  efrlim  26322  rlimcxp  26326  cxploglim2  26331  emcllem5  26352  zetacvg  26367  lgamgulmlem2  26382  lgamcvg2  26407  0sgmppw  26549  ppiub  26555  chtublem  26562  logfacrlim  26575  logexprlim  26576  chtppilimlem2  26825  rplogsumlem2  26836  dchrisumlem3  26842  dchrvmasumiflem1  26852  dchrisum0lem2  26869  selberg2lem  26901  logdivbnd  26907  pntrsumo1  26916  pntrlog2bndlem4  26931  pntpbnd1  26937  axlowdimlem17  27910  crctcshlem4  28768  clwlkclwwlklem2a1  28939  clwlkclwwlklem2a  28945  clwlkclwwlklem3  28948  clwlkclwwlk  28949  ipidsq  29655  nmcfnexi  30996  freshmansdream  32070  sgnsub  33147  knoppndvlem10  34987  poimirlem19  36100  poimirlem20  36101  ftc1anc  36162  cntotbnd  36258  aks4d1p1p2  40530  aks4d1p1p7  40534  irrapxlem3  41150  irrapxlem4  41151  pell14qrgt0  41185  pell1qrgaplem  41199  acongeq  41310  jm2.18  41315  hashnzfz  42607  hashnzfz2  42608  hashnzfzclim  42609  bccn1  42631  binomcxplemnotnn0  42643  dstregt0  43522  absimlere  43722  ellimcabssub0  43865  0ellimcdiv  43897  clim0cf  43902  fprodsubrecnncnvlem  44155  ioodvbdlimc2lem  44182  dvnxpaek  44190  dvnmul  44191  itgsbtaddcnst  44230  stoweidlem7  44255  stoweidlem11  44259  stoweidlem26  44274  dirkertrigeqlem2  44347  fourierdlem57  44411  fourierdlem60  44414  fourierdlem61  44415  fourierdlem68  44422  fourierdlem104  44458  fourierdlem107  44461  fourierdlem109  44463  etransclem4  44486  etransclem23  44505  etransclem27  44509  etransclem31  44513  etransclem35  44517  sigarexp  45107  sigaradd  45114  m1modmmod  46614  dignn0flhalflem1  46708  ehl2eudisval0  46818  2sphere0  46843  line2  46845  line2x  46847  itschlc0yqe  46853  itschlc0xyqsol1  46859  itschlc0xyqsol  46860
  Copyright terms: Public domain W3C validator