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	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( - 𝐴 = - 𝐵 ↔ 𝐴 = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		negeq	⊢ ( - 𝐴 = - 𝐵 → - - 𝐴 = - - 𝐵 )
2		negneg	⊢ ( 𝐴 ∈ ℂ → - - 𝐴 = 𝐴 )
3		negneg	⊢ ( 𝐵 ∈ ℂ → - - 𝐵 = 𝐵 )
4	2 3	eqeqan12d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( - - 𝐴 = - - 𝐵 ↔ 𝐴 = 𝐵 ) )
5	1 4	syl5ib	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( - 𝐴 = - 𝐵 → 𝐴 = 𝐵 ) )
6		negeq	⊢ ( 𝐴 = 𝐵 → - 𝐴 = - 𝐵 )
7	5 6	impbid1	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( - 𝐴 = - 𝐵 ↔ 𝐴 = 𝐵 ) )