Theorem eqresr

Description: Equality of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996) (New usage is discouraged.)

	Ref	Expression
Hypothesis	eqresr.1	$$⊢A\in \mathrm{V}$$
Assertion	eqresr	$$⊢⟨A,0_{𝑹}⟩=⟨B,0_{𝑹}⟩\leftrightarrow A=B$$

Proof

Step	Hyp	Ref	Expression
1		eqresr.1	$$⊢A\in \mathrm{V}$$
2		eqid	$$⊢0_{𝑹}=0_{𝑹}$$
3		0r	$$⊢0_{𝑹}\in 𝑹$$
4	3	elexi	$$⊢0_{𝑹}\in \mathrm{V}$$
5	1 4	opth	$$⊢⟨A,0_{𝑹}⟩=⟨B,0_{𝑹}⟩\leftrightarrow \left(A=B\wedge 0_{𝑹}=0_{𝑹}\right)$$
6	2 5	mpbiran2	$$⊢⟨A,0_{𝑹}⟩=⟨B,0_{𝑹}⟩\leftrightarrow A=B$$