Theorem 00id 8160

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

Syntax hints:   = wceq 1364   e. wcel 2164  (class class class)co 5918   CCcc 7870   0cc0 7872   + caddc 7875

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-ext 2175  ax-1cn 7965  ax-icn 7967  ax-addcl 7968  ax-mulcl 7970  ax-i2m1 7977  ax-0id 7980

This theorem depends on definitions:  df-bi 117  df-cleq 2186  df-clel 2189

This theorem is referenced by:  negdii  8303  addgt0  8467  addgegt0  8468  addgtge0  8469  addge0  8470  add20  8493  recexaplem2  8671  crap0  8977  iap0  9205  decaddm10  9506  10p10e20  9542  ser0  10604  bcpasc  10837  abs00ap  11206  fsumadd  11549  fsumrelem  11614  arisum  11641  bezoutr1  12170  nnnn0modprm0  12393  pcaddlem  12477  4sqlem19  12547  cnfld0  14059  1kp2ke3k  15216