Metamath Proof Explorer


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 )