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

Axiom ax-1rid 9016
Description:  1 is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, justified by theorem ax1rid 8992. Weakened from the original axiom in the form of statement in mulid1 9044, 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 8945 . . 3  class  RR
31, 2wcel 1721 . 2  wff  A  e.  RR
4 c1 8947 . . . 4  class  1
5 cmul 8951 . . . 4  class  x.
61, 4, 5co 6040 . . 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  9044  mulgt1  9825  ltmulgt11  9826  lemulge11  9828  addltmul  10159  xmulid1  10814  sqrlem7  12009  bezoutlem1  12993  nmopub2tALT  23365  nmfnleub2  23382  unitdivcld  24252  zrhre  24338  frghash2spot  28166  usgreghash2spotv  28169
  Copyright terms: Public domain W3C validator