Theorem 00id 7249

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

Syntax hints:   = wceq 1284   e. wcel 1433  (class class class)co 5532   CCcc 6979   0cc0 6981   + caddc 6984

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 1376  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-4 1440  ax-17 1459  ax-ial 1467  ax-ext 2063  ax-1cn 7069  ax-icn 7071  ax-addcl 7072  ax-mulcl 7074  ax-i2m1 7081  ax-0id 7084

This theorem depends on definitions:  df-bi 115  df-cleq 2074  df-clel 2077

This theorem is referenced by:  negdii  7392  addgt0  7552  addgegt0  7553  addgtge0  7554  addge0  7555  add20  7578  recexaplem2  7742  crap0  8035  iap0  8254  decaddm10  8535  10p10e20  8571  iser0  9471  bcpasc  9693  abs00ap  9948  bezoutr1  10422  1kp2ke3k  10562