Theorem subeq0bd

Description: If two complex numbers are equal, their difference is zero. Consequence of subeq0ad . Converse of subeq0d . Contrapositive of subne0ad . (Contributed by David Moews, 28-Feb-2017)

	Ref	Expression
Hypotheses	subeq0bd.1	$$⊢\phi \to A\in ℂ$$
	subeq0bd.2	$$⊢\phi \to A=B$$
Assertion	subeq0bd	$$⊢\phi \to A-B=0$$

Proof

Step	Hyp	Ref	Expression
1		subeq0bd.1	$$⊢\phi \to A\in ℂ$$
2		subeq0bd.2	$$⊢\phi \to A=B$$
3	2 1	eqeltrrd	$$⊢\phi \to B\in ℂ$$
4	1 3	subeq0ad	$$⊢\phi \to \left(A-B=0\leftrightarrow A=B\right)$$
5	2 4	mpbird	$$⊢\phi \to A-B=0$$