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 ) |
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 ) |