Axiom ax-0id 7882

Description: 0 is an identity element for real addition. Axiom for real and complex numbers, justified by Theorem ax0id 7840.

Proofs should normally use addid1 8057 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 16-Jan-2020.)

Assertion

Ref	Expression
ax-0id	⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)

Detailed syntax breakdown of Axiom ax-0id

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cc 7772	. . 3 class ℂ
3	1, 2	wcel 2141	. 2 wff 𝐴 ∈ ℂ
4		cc0 7774	. . . 4 class 0
5		caddc 7777	. . . 4 class +
6	1, 4, 5	co 5853	. . 3 class (𝐴 + 0)
7	6, 1	wceq 1348	. 2 wff (𝐴 + 0) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)

This axiom is referenced by:  addid1  8057