Axiom ax-rnegex

Description: Existence of negative of real number. Axiom 15 of 22 for real and complex numbers, justified by Theorem axrnegex . (Contributed by Eric Schmidt, 21-May-2007)

	Ref	Expression
Assertion	ax-rnegex	⊢ ( 𝐴 ∈ ℝ → ∃ 𝑥 ∈ ℝ ( 𝐴 + 𝑥 ) = 0 )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1		cr	⊢ ℝ
2	0 1	wcel	⊢ 𝐴 ∈ ℝ
3		vx	⊢ 𝑥
4		caddc	⊢ +
5	3	cv	⊢ 𝑥
6	0 5 4	co	⊢ ( 𝐴 + 𝑥 )
7		cc0	⊢ 0
8	6 7	wceq	⊢ ( 𝐴 + 𝑥 ) = 0
9	8 3 1	wrex	⊢ ∃ 𝑥 ∈ ℝ ( 𝐴 + 𝑥 ) = 0
10	2 9	wi	⊢ ( 𝐴 ∈ ℝ → ∃ 𝑥 ∈ ℝ ( 𝐴 + 𝑥 ) = 0 )