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

Axiom ax-1rid 8823
Description:  1 is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, justified by theorem ax1rid 8799. Weakened from the original axiom in the form of statement in mulid1 8851, 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 8752 . . 3  class  RR
31, 2wcel 1696 . 2  wff  A  e.  RR
4 c1 8754 . . . 4  class  1
5 cmul 8758 . . . 4  class  x.
61, 4, 5co 5874 . . 3  class  ( A  x.  1 )
76, 1wceq 1632 . 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  8851  mulgt1  9631  ltmulgt11  9632  lemulge11  9634  addltmul  9963  xmulid1  10615  sqrlem7  11750  bezoutlem1  12733  nmopub2tALT  22505  nmfnleub2  22522  unitdivcld  23300
  Copyright terms: Public domain W3C validator