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

Axiom ax-1rid 9885
 Description: 1 is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, justified by theorem ax1rid 9861. Weakened from the original axiom in the form of statement in mulid1 9916, 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 9814 . . 3 class
31, 2wcel 1977 . 2 wff 𝐴 ∈ ℝ
4 c1 9816 . . . 4 class 1
5 cmul 9820 . . . 4 class ·
61, 4, 5co 6549 . . 3 class (𝐴 · 1)
76, 1wceq 1475 . 2 wff (𝐴 · 1) = 𝐴
83, 7wi 4 1 wff (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴)
 Colors of variables: wff setvar class This axiom is referenced by:  mulid1  9916  mulgt1  10761  ltmulgt11  10762  lemulge11  10764  addltmul  11145  xmulid1  11981  2submod  12593  cshw1  13419  bezoutlem1  15094  cshwshashnsame  15648  frghash2spot  26590  usgreghash2spotv  26593  numclwwlk6  26640  nmopub2tALT  28152  nmfnleub2  28169  unitdivcld  29275  zrhre  29391  sgnmulrp2  29932  knoppcnlem4  31656  relexpmulnn  37020  frgrhash2wsp  41497  fusgreghash2wspv  41499  av-numclwwlk6  41544  relogbmulbexp  42153
 Copyright terms: Public domain W3C validator