Theorem 00id 8319

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 8170	. 2 |- 0 e. CC
2		addrid 8316	. 2 |- ( 0 e. CC -> ( 0 + 0 ) = 0 )
3	1, 2	ax-mp 5	1 |- ( 0 + 0 ) = 0

Syntax hints:   = wceq 1397   e. wcel 2202  (class class class)co 6017   CCcc 8029   0cc0 8031   + caddc 8034

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-ext 2213  ax-1cn 8124  ax-icn 8126  ax-addcl 8127  ax-mulcl 8129  ax-i2m1 8136  ax-0id 8139

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227

This theorem is referenced by:  negdii  8462  addgt0  8627  addgegt0  8628  addgtge0  8629  addge0  8630  add20  8653  recexaplem2  8831  crap0  9137  iap0  9366  decaddm10  9668  10p10e20  9704  ser0  10794  bcpasc  11027  abs00ap  11622  fsumadd  11966  fsumrelem  12031  arisum  12058  bezoutr1  12603  nnnn0modprm0  12827  pcaddlem  12911  4sqlem19  12981  cnfld0  14584  vtxdgfi0e  16145  1kp2ke3k  16320