Metamath Proof Explorer


Axiom ax-1rid

Description: 1 is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, justified by Theorem ax1rid . Weakened from the original axiom in the form of statement in mulid1 , based on ideas by Eric Schmidt. (Contributed by NM, 29-Jan-1995)

Ref Expression
Assertion ax-1rid
|- ( A e. RR -> ( A x. 1 ) = A )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA
 |-  A
1 cr
 |-  RR
2 0 1 wcel
 |-  A e. RR
3 cmul
 |-  x.
4 c1
 |-  1
5 0 4 3 co
 |-  ( A x. 1 )
6 5 0 wceq
 |-  ( A x. 1 ) = A
7 2 6 wi
 |-  ( A e. RR -> ( A x. 1 ) = A )