![]() |
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 6763. (Contributed by Eric Schmidt, 21-May-2007.) |
Ref | Expression |
---|---|
ax-rnegex | ⊢ (A ∈ ℝ → ∃x ∈ ℝ (A + x) = 0) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class A | |
2 | cr 6710 | . . 3 class ℝ | |
3 | 1, 2 | wcel 1390 | . 2 wff A ∈ ℝ |
4 | vx | . . . . . 6 setvar x | |
5 | 4 | cv 1241 | . . . . 5 class x |
6 | caddc 6714 | . . . . 5 class + | |
7 | 1, 5, 6 | co 5455 | . . . 4 class (A + x) |
8 | cc0 6711 | . . . 4 class 0 | |
9 | 7, 8 | wceq 1242 | . . 3 wff (A + x) = 0 |
10 | 9, 4, 2 | wrex 2301 | . 2 wff ∃x ∈ ℝ (A + x) = 0 |
11 | 3, 10 | wi 4 | 1 wff (A ∈ ℝ → ∃x ∈ ℝ (A + x) = 0) |
Colors of variables: wff set class |
This axiom is referenced by: 0re 6825 readdcan 6950 cnegexlem1 6983 cnegexlem2 6984 cnegexlem3 6985 cnegex 6986 renegcl 7068 ltadd2 7212 |
Copyright terms: Public domain | W3C validator |