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

Axiom ax-1rid 9020
Description:  1 is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, justified by theorem ax1rid 8996. Weakened from the original axiom in the form of statement in mulid1 9048, 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 8949 . . 3  class  RR
31, 2wcel 1721 . 2  wff  A  e.  RR
4 c1 8951 . . . 4  class  1
5 cmul 8955 . . . 4  class  x.
61, 4, 5co 6044 . . 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  9048  mulgt1  9829  ltmulgt11  9830  lemulge11  9832  addltmul  10163  xmulid1  10818  sqrlem7  12013  bezoutlem1  12997  nmopub2tALT  23369  nmfnleub2  23386  unitdivcld  24256  zrhre  24342  frghash2spot  28170  usgreghash2spotv  28173
  Copyright terms: Public domain W3C validator