Theorem repncan2

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

	Ref	Expression
Assertion	repncan2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 + 𝐵 ) −ℝ 𝐴 ) = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( 𝐴 + 𝐵 ) = ( 𝐴 + 𝐵 )
2		readdcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 + 𝐵 ) ∈ ℝ )
3		simpl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐴 ∈ ℝ )
4		simpr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐵 ∈ ℝ )
5	2 3 4	resubaddd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( ( 𝐴 + 𝐵 ) −ℝ 𝐴 ) = 𝐵 ↔ ( 𝐴 + 𝐵 ) = ( 𝐴 + 𝐵 ) ) )
6	1 5	mpbiri	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 + 𝐵 ) −ℝ 𝐴 ) = 𝐵 )