Theorem subeq0

Description: If the difference between two numbers is zero, they are equal. (Contributed by NM, 16-Nov-1999)

	Ref	Expression
Assertion	subeq0	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(A-B=0\leftrightarrow A=B\right)$$

Proof

Step	Hyp	Ref	Expression
1		subid	$$⊢B\in ℂ\to B-B=0$$
2	1	adantl	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to B-B=0$$
3	2	eqeq2d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(A-B=B-B\leftrightarrow A-B=0\right)$$
4		subcan2	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge B\in ℂ\right)\to \left(A-B=B-B\leftrightarrow A=B\right)$$
5	4	3anidm23	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(A-B=B-B\leftrightarrow A=B\right)$$
6	3 5	bitr3d	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(A-B=0\leftrightarrow A=B\right)$$