MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax-1rid Unicode version

Axiom ax-1rid 8993
Description:  1 is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, justified by theorem ax1rid 8969. Weakened from the original axiom in the form of statement in mulid1 9021, based on ideas by Eric Schmidt. (Contributed by NM, 29-Jan-1995.)
Assertion
Ref Expression
ax-1rid  |-  ( A  e.  RR  ->  ( A  x.  1 )  =  A )

Detailed syntax breakdown of Axiom ax-1rid
StepHypRef Expression
1 cA . . 3  class  A
2 cr 8922 . . 3  class  RR
31, 2wcel 1717 . 2  wff  A  e.  RR
4 c1 8924 . . . 4  class  1
5 cmul 8928 . . . 4  class  x.
61, 4, 5co 6020 . . 3  class  ( A  x.  1 )
76, 1wceq 1649 . 2  wff  ( A  x.  1 )  =  A
83, 7wi 4 1  wff  ( A  e.  RR  ->  ( A  x.  1 )  =  A )
Colors of variables: wff set class
This axiom is referenced by:  mulid1  9021  mulgt1  9801  ltmulgt11  9802  lemulge11  9804  addltmul  10135  xmulid1  10790  sqrlem7  11981  bezoutlem1  12965  nmopub2tALT  23260  nmfnleub2  23277  unitdivcld  24103  zrhre  24181
  Copyright terms: Public domain W3C validator