![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ax-rnegex | Structured version Visualization version GIF version |
Description: Existence of negative of real number. Axiom 15 of 22 for real and complex numbers, justified by theorem axrnegex 10380. (Contributed by Eric Schmidt, 21-May-2007.) |
Ref | Expression |
---|---|
ax-rnegex | ⊢ (𝐴 ∈ ℝ → ∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | cr 10332 | . . 3 class ℝ | |
3 | 1, 2 | wcel 2050 | . 2 wff 𝐴 ∈ ℝ |
4 | vx | . . . . . 6 setvar 𝑥 | |
5 | 4 | cv 1506 | . . . . 5 class 𝑥 |
6 | caddc 10336 | . . . . 5 class + | |
7 | 1, 5, 6 | co 6974 | . . . 4 class (𝐴 + 𝑥) |
8 | cc0 10333 | . . . 4 class 0 | |
9 | 7, 8 | wceq 1507 | . . 3 wff (𝐴 + 𝑥) = 0 |
10 | 9, 4, 2 | wrex 3083 | . 2 wff ∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0 |
11 | 3, 10 | wi 4 | 1 wff (𝐴 ∈ ℝ → ∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0) |
Colors of variables: wff setvar class |
This axiom is referenced by: 0re 10439 0reOLD 10440 00id 10613 addid1 10618 cnegex 10619 0cnALT 10672 renegcli 10746 elre0re 38620 renegeu 38661 |
Copyright terms: Public domain | W3C validator |