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

Axiom ax-1rid 9098
Description:  1 is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, justified by theorem ax1rid 9074. Weakened from the original axiom in the form of statement in mulid1 9126, 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 9027 . . 3  class  RR
31, 2wcel 1728 . 2  wff  A  e.  RR
4 c1 9029 . . . 4  class  1
5 cmul 9033 . . . 4  class  x.
61, 4, 5co 6117 . . 3  class  ( A  x.  1 )
76, 1wceq 1654 . 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  9126  mulgt1  9907  ltmulgt11  9908  lemulge11  9910  addltmul  10241  xmulid1  10896  sqrlem7  12092  bezoutlem1  13076  nmopub2tALT  23450  nmfnleub2  23467  unitdivcld  24334  zrhre  24420  2submod  28273  cshw1  28407  cshwssizensame  28421  frghash2spot  28624  usgreghash2spotv  28627
  Copyright terms: Public domain W3C validator