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

Metamath Proof Explorer

Theorem repncan2

Description: Addition and subtraction of equals. Compare pncan2 . (Contributed by Steven Nguyen, 8-Jan-2023)

		Ref	Expression
	Assertion	repncan2	$⊢ (A \in ℝ \land B \in ℝ) \to (A + B) -_{ℝ} A = B$

Step	Hyp	Ref	Expression
1		eqid	$⊢ A + B = A + B$
2		readdcl	$⊢ (A \in ℝ \land B \in ℝ) \to A + B \in ℝ$
3		simpl	$⊢ (A \in ℝ \land B \in ℝ) \to A \in ℝ$
4		simpr	$⊢ (A \in ℝ \land B \in ℝ) \to B \in ℝ$
5	2 3 4	resubaddd	$⊢ (A \in ℝ \land B \in ℝ) \to ((A + B) -_{ℝ} A = B \leftrightarrow A + B = A + B)$
6	1 5	mpbiri	$⊢ (A \in ℝ \land B \in ℝ) \to (A + B) -_{ℝ} A = B$