This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	subeq0bd.2	⊢ ( 𝜑 → 𝐴 = 𝐵 )
Assertion	subeq0bd	⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		subeq0bd.1	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2		subeq0bd.2	⊢ ( 𝜑 → 𝐴 = 𝐵 )
3	2 1	eqeltrrd	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
4	1 3	subeq0ad	⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) = 0 ↔ 𝐴 = 𝐵 ) )
5	2 4	mpbird	⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) = 0 )