![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ax-rnegex | GIF version |
Description: Existence of negative of real number. Axiom for real and complex numbers, justified by Theorem axrnegex 7877. (Contributed by Eric Schmidt, 21-May-2007.) |
Ref | Expression |
---|---|
ax-rnegex | ⊢ (𝐴 ∈ ℝ → ∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | cr 7809 | . . 3 class ℝ | |
3 | 1, 2 | wcel 2148 | . 2 wff 𝐴 ∈ ℝ |
4 | vx | . . . . . 6 setvar 𝑥 | |
5 | 4 | cv 1352 | . . . . 5 class 𝑥 |
6 | caddc 7813 | . . . . 5 class + | |
7 | 1, 5, 6 | co 5874 | . . . 4 class (𝐴 + 𝑥) |
8 | cc0 7810 | . . . 4 class 0 | |
9 | 7, 8 | wceq 1353 | . . 3 wff (𝐴 + 𝑥) = 0 |
10 | 9, 4, 2 | wrex 2456 | . 2 wff ∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0 |
11 | 3, 10 | wi 4 | 1 wff (𝐴 ∈ ℝ → ∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0) |
Colors of variables: wff set class |
This axiom is referenced by: 0re 7956 readdcan 8095 cnegexlem1 8130 cnegexlem2 8131 cnegexlem3 8132 cnegex 8133 renegcl 8216 ltadd2 8374 |
Copyright terms: Public domain | W3C validator |