This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xneg11

Description: Extended real version of neg11 . (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xneg11 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → − A = − B ↔ A = B

Proof

Step Hyp Ref Expression
1 xnegeq ⊢ − A = − B → − − A = − − B
2 xnegneg ⊢ A ∈ ℝ * → − − A = A
3 xnegneg ⊢ B ∈ ℝ * → − − B = B
4 2 3 eqeqan12d ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → − − A = − − B ↔ A = B
5 1 4 imbitrid ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → − A = − B → A = B
6 xnegeq ⊢ A = B → − A = − B
7 5 6 impbid1 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → − A = − B ↔ A = B