Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ax-0id | Unicode version |
Description: is an identity element for real addition. Axiom
for real and
complex numbers, justified by theorem ax0id 7679.
Proofs should normally use addid1 7893 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 16-Jan-2020.) |
Ref | Expression |
---|---|
ax-0id |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 | |
2 | cc 7611 | . . 3 | |
3 | 1, 2 | wcel 1480 | . 2 |
4 | cc0 7613 | . . . 4 | |
5 | caddc 7616 | . . . 4 | |
6 | 1, 4, 5 | co 5767 | . . 3 |
7 | 6, 1 | wceq 1331 | . 2 |
8 | 3, 7 | wi 4 | 1 |
Colors of variables: wff set class |
This axiom is referenced by: addid1 7893 |
Copyright terms: Public domain | W3C validator |