![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ax-0id | GIF version |
Description: 0
is an identity element for real addition. Axiom for real and
complex numbers, justified by Theorem ax0id 7879.
Proofs should normally use addid1 8097 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 16-Jan-2020.) |
Ref | Expression |
---|---|
ax-0id | ⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | cc 7811 | . . 3 class ℂ | |
3 | 1, 2 | wcel 2148 | . 2 wff 𝐴 ∈ ℂ |
4 | cc0 7813 | . . . 4 class 0 | |
5 | caddc 7816 | . . . 4 class + | |
6 | 1, 4, 5 | co 5877 | . . 3 class (𝐴 + 0) |
7 | 6, 1 | wceq 1353 | . 2 wff (𝐴 + 0) = 𝐴 |
8 | 3, 7 | wi 4 | 1 wff (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴) |
Colors of variables: wff set class |
This axiom is referenced by: addid1 8097 |
Copyright terms: Public domain | W3C validator |