Theorem 00id 8362

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

Syntax hints:   = wceq 1398   e. wcel 2202  (class class class)co 6028   CCcc 8073   0cc0 8075   + caddc 8078

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2213  ax-1cn 8168  ax-icn 8170  ax-addcl 8171  ax-mulcl 8173  ax-i2m1 8180  ax-0id 8183

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227

This theorem is referenced by:  negdii  8505  addgt0  8670  addgegt0  8671  addgtge0  8672  addge0  8673  add20  8696  recexaplem2  8874  crap0  9180  iap0  9409  decaddm10  9713  10p10e20  9749  ser0  10841  bcpasc  11074  abs00ap  11685  fsumadd  12030  fsumrelem  12095  arisum  12122  bezoutr1  12667  nnnn0modprm0  12891  pcaddlem  12975  4sqlem19  13045  cnfld0  14650  vtxdgfi0e  16219  1kp2ke3k  16421