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

Metamath Proof Explorer

Theorem neg11

Description: Negative is one-to-one. (Contributed by NM, 8-Feb-2005) (Revised by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion neg11 ⊢ A ∈ ℂ ∧ B ∈ ℂ → − A = − B ↔ A = B

Proof

Step Hyp Ref Expression
1 negeq ⊢ − A = − B → − − A = − − B
2 negneg ⊢ A ∈ ℂ → − − A = A
3 negneg ⊢ B ∈ ℂ → − − B = B
4 2 3 eqeqan12d ⊢ A ∈ ℂ ∧ B ∈ ℂ → − − A = − − B ↔ A = B
5 1 4 imbitrid ⊢ A ∈ ℂ ∧ B ∈ ℂ → − A = − B → A = B
6 negeq ⊢ A = B → − A = − B
7 5 6 impbid1 ⊢ A ∈ ℂ ∧ B ∈ ℂ → − A = − B ↔ A = B