This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Metamath Proof Explorer
Theorem 1pr
Description: The positive real number 'one'. (Contributed by NM, 13-Mar-1996)
(Revised by Mario Carneiro, 12-Jun-2013) (New usage is discouraged.)
|
|
Ref |
Expression |
|
Assertion |
1pr |
|- 1P e. P. |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
df-1p |
|- 1P = { x | x |
| 2 |
|
1nq |
|- 1Q e. Q. |
| 3 |
|
nqpr |
|- ( 1Q e. Q. -> { x | x |
| 4 |
2 3
|
ax-mp |
|- { x | x |
| 5 |
1 4
|
eqeltri |
|- 1P e. P. |