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

Axiom ax-1rid 9694
Description: 1 is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, justified by theorem ax1rid 9670. Weakened from the original axiom in the form of statement in mulid1 9725, based on ideas by Eric Schmidt. (Contributed by NM, 29-Jan-1995.)
Assertion
Ref Expression
ax-1rid (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴)

Detailed syntax breakdown of Axiom ax-1rid
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cr 9623 . . 3 class
31, 2wcel 1937 . 2 wff 𝐴 ∈ ℝ
4 c1 9625 . . . 4 class 1
5 cmul 9629 . . . 4 class ·
61, 4, 5co 6363 . . 3 class (𝐴 · 1)
76, 1wceq 1468 . 2 wff (𝐴 · 1) = 𝐴
83, 7wi 4 1 wff (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴)
Colors of variables: wff setvar class
This axiom is referenced by:  mulid1  9725  mulgt1  10553  ltmulgt11  10554  lemulge11  10556  addltmul  10938  xmulid1  11660  2submod  12260  cshw1  13057  bezoutlem1  14665  cshwshashnsame  15235  frghash2spot  25951  usgreghash2spotv  25954  numclwwlk6  26001  nmopub2tALT  27725  nmfnleub2  27742  unitdivcld  28862  zrhre  28978  sgnmulrp2  29568  knoppcnlem4  31294  relexpmulnn  36540  frgrhash2wsp  40897  fusgreghash2wspv  40899  av-numclwwlk6  40944  relogbmulbexp  41561
  Copyright terms: Public domain W3C validator