Theorem 00id 7903

Description: 0 is its own additive identity. (Contributed by Scott Fenton, 3-Jan-2013.)

Assertion

Ref	Expression
00id	|- ( 0 + 0 ) = 0

Proof of Theorem 00id

Step	Hyp	Ref	Expression
1		0cn 7758	. 2 |- 0 e. CC
2		addid1 7900	. 2 |- ( 0 e. CC -> ( 0 + 0 ) = 0 )
3	1, 2	ax-mp 5	1 |- ( 0 + 0 ) = 0

Syntax hints:   = wceq 1331   e. wcel 1480  (class class class)co 5774   CCcc 7618   0cc0 7620   + caddc 7623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-ext 2121  ax-1cn 7713  ax-icn 7715  ax-addcl 7716  ax-mulcl 7718  ax-i2m1 7725  ax-0id 7728

This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-clel 2135

This theorem is referenced by:  negdii  8046  addgt0  8210  addgegt0  8211  addgtge0  8212  addge0  8213  add20  8236  recexaplem2  8413  crap0  8716  iap0  8943  decaddm10  9240  10p10e20  9276  ser0  10287  bcpasc  10512  abs00ap  10834  fsumadd  11175  fsumrelem  11240  arisum  11267  bezoutr1  11721  1kp2ke3k  12936