Theorem 00id 7621

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 7478	. 2 |- 0 e. CC
2		addid1 7618	. 2 |- ( 0 e. CC -> ( 0 + 0 ) = 0 )
3	1, 2	ax-mp 7	1 |- ( 0 + 0 ) = 0

Syntax hints:   = wceq 1289   e. wcel 1438  (class class class)co 5652   CCcc 7346   0cc0 7348   + caddc 7351

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445  ax-17 1464  ax-ial 1472  ax-ext 2070  ax-1cn 7436  ax-icn 7438  ax-addcl 7439  ax-mulcl 7441  ax-i2m1 7448  ax-0id 7451

This theorem depends on definitions:  df-bi 115  df-cleq 2081  df-clel 2084

This theorem is referenced by:  negdii  7764  addgt0  7924  addgegt0  7925  addgtge0  7926  addge0  7927  add20  7950  recexaplem2  8119  crap0  8416  iap0  8637  decaddm10  8933  10p10e20  8969  iser0  9943  ser0  9945  bcpasc  10170  abs00ap  10491  fsumadd  10796  fsumrelem  10861  arisum  10888  bezoutr1  11296  1kp2ke3k  11606