Metamath Proof Explorer

Theorem enrbreq

Description: Equivalence relation for signed reals in terms of positive reals. (Contributed by NM, 3-Sep-1995) (New usage is discouraged.)

		Ref	Expression
	Assertion	enrbreq	$⊢ ((A \in 𝑷 \land B \in 𝑷) \land (C \in 𝑷 \land D \in 𝑷)) \to (⟨A, B⟩ ~_{𝑹} ⟨C, D⟩ \leftrightarrow A +_{𝑷} D = B +_{𝑷} C)$

Step	Hyp	Ref	Expression
1		df-enr	$⊢ ~_{𝑹} = \{⟨x, y⟩ \| ((x \in (𝑷 \times 𝑷) \land y \in (𝑷 \times 𝑷)) \land \exists z \exists w \exists v \exists u ((x = ⟨z, w⟩ \land y = ⟨v, u⟩) \land z +_{𝑷} u = w +_{𝑷} v))\}$
2	1	ecopoveq	$⊢ ((A \in 𝑷 \land B \in 𝑷) \land (C \in 𝑷 \land D \in 𝑷)) \to (⟨A, B⟩ ~_{𝑹} ⟨C, D⟩ \leftrightarrow A +_{𝑷} D = B +_{𝑷} C)$