Description: Extended real version of neg11 . (Contributed by Mario Carneiro, 20-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | xneg11 | ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( -𝑒 𝐴 = -𝑒 𝐵 ↔ 𝐴 = 𝐵 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xnegeq | ⊢ ( -𝑒 𝐴 = -𝑒 𝐵 → -𝑒 -𝑒 𝐴 = -𝑒 -𝑒 𝐵 ) | |
2 | xnegneg | ⊢ ( 𝐴 ∈ ℝ* → -𝑒 -𝑒 𝐴 = 𝐴 ) | |
3 | xnegneg | ⊢ ( 𝐵 ∈ ℝ* → -𝑒 -𝑒 𝐵 = 𝐵 ) | |
4 | 2 3 | eqeqan12d | ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( -𝑒 -𝑒 𝐴 = -𝑒 -𝑒 𝐵 ↔ 𝐴 = 𝐵 ) ) |
5 | 1 4 | syl5ib | ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( -𝑒 𝐴 = -𝑒 𝐵 → 𝐴 = 𝐵 ) ) |
6 | xnegeq | ⊢ ( 𝐴 = 𝐵 → -𝑒 𝐴 = -𝑒 𝐵 ) | |
7 | 5 6 | impbid1 | ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( -𝑒 𝐴 = -𝑒 𝐵 ↔ 𝐴 = 𝐵 ) ) |