Theorem 00id 8213

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

Syntax hints:   = wceq 1373   e. wcel 2176  (class class class)co 5944   CCcc 7923   0cc0 7925   + caddc 7928

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-ext 2187  ax-1cn 8018  ax-icn 8020  ax-addcl 8021  ax-mulcl 8023  ax-i2m1 8030  ax-0id 8033

This theorem depends on definitions:  df-bi 117  df-cleq 2198  df-clel 2201

This theorem is referenced by:  negdii  8356  addgt0  8521  addgegt0  8522  addgtge0  8523  addge0  8524  add20  8547  recexaplem2  8725  crap0  9031  iap0  9260  decaddm10  9562  10p10e20  9598  ser0  10678  bcpasc  10911  abs00ap  11373  fsumadd  11717  fsumrelem  11782  arisum  11809  bezoutr1  12354  nnnn0modprm0  12578  pcaddlem  12662  4sqlem19  12732  cnfld0  14333  1kp2ke3k  15660