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 e. _V
Assertion	eqresr	|- ( <. A , 0R >. = <. B , 0R >. <-> A = B )

Proof

Step	Hyp	Ref	Expression
1		eqresr.1	|- A e. _V
2		eqid	|- 0R = 0R
3		0r	|- 0R e. R.
4	3	elexi	|- 0R e. _V
5	1 4	opth	|- ( <. A , 0R >. = <. B , 0R >. <-> ( A = B /\ 0R = 0R ) )
6	2 5	mpbiran2	|- ( <. A , 0R >. = <. B , 0R >. <-> A = B )