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

Axiom ax-1rid 9060
Description:  1 is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, justified by theorem ax1rid 9036. Weakened from the original axiom in the form of statement in mulid1 9088, 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 8989 . . 3  class  RR
31, 2wcel 1725 . 2  wff  A  e.  RR
4 c1 8991 . . . 4  class  1
5 cmul 8995 . . . 4  class  x.
61, 4, 5co 6081 . . 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  9088  mulgt1  9869  ltmulgt11  9870  lemulge11  9872  addltmul  10203  xmulid1  10858  sqrlem7  12054  bezoutlem1  13038  nmopub2tALT  23412  nmfnleub2  23429  unitdivcld  24299  zrhre  24385  2submod  28152  cshw1  28275  cshwssizensame  28289  frghash2spot  28452  usgreghash2spotv  28455
  Copyright terms: Public domain W3C validator