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

Axiom ax-1rid 9049
Description:  1 is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, justified by theorem ax1rid 9025. Weakened from the original axiom in the form of statement in mulid1 9077, 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 8978 . . 3  class  RR
31, 2wcel 1725 . 2  wff  A  e.  RR
4 c1 8980 . . . 4  class  1
5 cmul 8984 . . . 4  class  x.
61, 4, 5co 6072 . . 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  9077  mulgt1  9858  ltmulgt11  9859  lemulge11  9861  addltmul  10192  xmulid1  10847  sqrlem7  12042  bezoutlem1  13026  nmopub2tALT  23400  nmfnleub2  23417  unitdivcld  24287  zrhre  24373  2submod  28058  shwrd1  28161  shwrdssizensame  28174  frghash2spot  28310  usgreghash2spotv  28313
  Copyright terms: Public domain W3C validator