Theorem 00id 8098

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

Syntax hints:   = wceq 1353   e. wcel 2148  (class class class)co 5875   CCcc 7809   0cc0 7811   + caddc 7814

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159  ax-1cn 7904  ax-icn 7906  ax-addcl 7907  ax-mulcl 7909  ax-i2m1 7916  ax-0id 7919

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173

This theorem is referenced by:  negdii  8241  addgt0  8405  addgegt0  8406  addgtge0  8407  addge0  8408  add20  8431  recexaplem2  8609  crap0  8915  iap0  9142  decaddm10  9442  10p10e20  9478  ser0  10514  bcpasc  10746  abs00ap  11071  fsumadd  11414  fsumrelem  11479  arisum  11506  bezoutr1  12034  nnnn0modprm0  12255  pcaddlem  12338  cnfld0  13468  1kp2ke3k  14479