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

Metamath Proof Explorer

Theorem subid

Description: Subtraction of a number from itself. (Contributed by NM, 8-Oct-1999) (Revised by Mario Carneiro, 27-May-2016)

		Ref	Expression
	Assertion	subid	$⊢ A \in ℂ \to A - A = 0$

Step	Hyp	Ref	Expression
1		addrid	$⊢ A \in ℂ \to A + 0 = A$
2	1	oveq1d	$⊢ A \in ℂ \to A + 0 - A = A - A$
3		0cn	$⊢ 0 \in ℂ$
4		pncan2	$⊢ (A \in ℂ \land 0 \in ℂ) \to A + 0 - A = 0$
5	3 4	mpan2	$⊢ A \in ℂ \to A + 0 - A = 0$
6	2 5	eqtr3d	$⊢ A \in ℂ \to A - A = 0$