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

Axiom ax-1rid 9052
Description:  1 is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, justified by theorem ax1rid 9028. Weakened from the original axiom in the form of statement in mulid1 9080, 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 8981 . . 3  class  RR
31, 2wcel 1725 . 2  wff  A  e.  RR
4 c1 8983 . . . 4  class  1
5 cmul 8987 . . . 4  class  x.
61, 4, 5co 6073 . . 3  class  ( A  x.  1 )
76, 1wceq 1652 . 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  9080  mulgt1  9861  ltmulgt11  9862  lemulge11  9864  addltmul  10195  xmulid1  10850  sqrlem7  12046  bezoutlem1  13030  nmopub2tALT  23404  nmfnleub2  23421  unitdivcld  24291  zrhre  24377  2submod  28130  cshw1  28238  cshwssizensame  28252  frghash2spot  28389  usgreghash2spotv  28392
  Copyright terms: Public domain W3C validator