Metamath Proof Explorer


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 )