Theorem 00id 7896

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 7751	. 2 |- 0 e. CC
2		addid1 7893	. 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 5767   CCcc 7611   0cc0 7613   + caddc 7616

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 2119  ax-1cn 7706  ax-icn 7708  ax-addcl 7709  ax-mulcl 7711  ax-i2m1 7718  ax-0id 7721

This theorem depends on definitions:  df-bi 116  df-cleq 2130  df-clel 2133

This theorem is referenced by:  negdii  8039  addgt0  8203  addgegt0  8204  addgtge0  8205  addge0  8206  add20  8229  recexaplem2  8406  crap0  8709  iap0  8936  decaddm10  9233  10p10e20  9269  ser0  10280  bcpasc  10505  abs00ap  10827  fsumadd  11168  fsumrelem  11233  arisum  11260  bezoutr1  11710  1kp2ke3k  12925