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	|- ( ph -> A e. CC )
	subeq0bd.2	|- ( ph -> A = B )
Assertion	subeq0bd	|- ( ph -> ( A - B ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		subeq0bd.1	|- ( ph -> A e. CC )
2		subeq0bd.2	|- ( ph -> A = B )
3	2 1	eqeltrrd	|- ( ph -> B e. CC )
4	1 3	subeq0ad	|- ( ph -> ( ( A - B ) = 0 <-> A = B ) )
5	2 4	mpbird	|- ( ph -> ( A - B ) = 0 )