Theorem 00id 8457

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

Syntax hints:   = wceq 1402   e. wcel 2209  (class class class)co 6075   CCcc 8167   0cc0 8169   + caddc 8172

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220  ax-1cn 8262  ax-icn 8264  ax-addcl 8265  ax-mulcl 8267  ax-i2m1 8274  ax-0id 8277

This theorem depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is referenced by:  negdii  8600  addgt0  8766  addgegt0  8767  addgtge0  8768  addge0  8769  add20  8792  recexaplem2  8970  crap0  9278  iap0  9507  decaddm10  9814  10p10e20  9850  ser0  10948  bcpasc  11182  abs00ap  11806  fsumadd  12151  fsumrelem  12216  arisum  12243  bezoutr1  12788  nnnn0modprm0  13012  pcaddlem  13096  4sqlem19  13166  cnfld0  14880  vtxdgfi0e  16450  1kp2ke3k  16652