Metamath Proof Explorer
Description: Alternate proof of 1t1e1 using a different set of axioms (add
ax-mulrcl , ax-i2m1 , ax-1ne0 , ax-rrecex and remove ax-resscn ,
ax-mulcom , ax-mulass , ax-distr ). (Contributed by Steven Nguyen, 20-Sep-2022) (Proof modification is discouraged.)
(New usage is discouraged.)
|
|
Ref |
Expression |
|
Assertion |
1t1e1ALT |
|- ( 1 x. 1 ) = 1 |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
1re |
|- 1 e. RR |
| 2 |
|
ax-1rid |
|- ( 1 e. RR -> ( 1 x. 1 ) = 1 ) |
| 3 |
1 2
|
ax-mp |
|- ( 1 x. 1 ) = 1 |