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

Metamath Proof Explorer

Theorem subid1

Description: Identity law for subtraction. (Contributed by NM, 9-May-2004) (Revised by Mario Carneiro, 27-May-2016)

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

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