Metamath Proof Explorer

Theorem subeqrev

Description: Reverse the order of subtraction in an equality. (Contributed by Scott Fenton, 8-Jul-2013)

Ref Expression
Assertion subeqrev ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A − B = C − D ↔ B − A = D − C

Proof

Step Hyp Ref Expression
1 subcl ⊢ A ∈ ℂ ∧ B ∈ ℂ → A − B ∈ ℂ
2 subcl ⊢ C ∈ ℂ ∧ D ∈ ℂ → C − D ∈ ℂ
3 neg11 ⊢ A − B ∈ ℂ ∧ C − D ∈ ℂ → − A − B = − C − D ↔ A − B = C − D
4 1 2 3 syl2an ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → − A − B = − C − D ↔ A − B = C − D
5 negsubdi2 ⊢ A ∈ ℂ ∧ B ∈ ℂ → − A − B = B − A
6 negsubdi2 ⊢ C ∈ ℂ ∧ D ∈ ℂ → − C − D = D − C
7 5 6 eqeqan12d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → − A − B = − C − D ↔ B − A = D − C
8 4 7 bitr3d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A − B = C − D ↔ B − A = D − C