Metamath Proof Explorer
Description: If the difference between two numbers is zero, they are equal.
(Contributed by NM, 8May1999)


Ref 
Expression 

Hypotheses 
negidi.1 
⊢ 𝐴 ∈ ℂ 


pncan3i.2 
⊢ 𝐵 ∈ ℂ 

Assertion 
subeq0i 
⊢ ( ( 𝐴 − 𝐵 ) = 0 ↔ 𝐴 = 𝐵 ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

negidi.1 
⊢ 𝐴 ∈ ℂ 
2 

pncan3i.2 
⊢ 𝐵 ∈ ℂ 
3 

subeq0 
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 − 𝐵 ) = 0 ↔ 𝐴 = 𝐵 ) ) 
4 
1 2 3

mp2an 
⊢ ( ( 𝐴 − 𝐵 ) = 0 ↔ 𝐴 = 𝐵 ) 