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 9950
Description: 1 is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, justified by theorem ax1rid 9926. Weakened from the original axiom in the form of statement in mulid1 9981, 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 9879 . . 3 class
31, 2wcel 1987 . 2 wff 𝐴 ∈ ℝ
4 c1 9881 . . . 4 class 1
5 cmul 9885 . . . 4 class ·
61, 4, 5co 6604 . . 3 class (𝐴 · 1)
76, 1wceq 1480 . 2 wff (𝐴 · 1) = 𝐴
83, 7wi 4 1 wff (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴)
Colors of variables: wff setvar class
This axiom is referenced by:  mulid1  9981  mulgt1  10826  ltmulgt11  10827  lemulge11  10829  addltmul  11212  xmulid1  12052  2submod  12671  cshw1  13505  bezoutlem1  15180  cshwshashnsame  15734  frgrhash2wsp  27055  fusgreghash2wspv  27057  numclwwlk6  27102  nmopub2tALT  28614  nmfnleub2  28631  unitdivcld  29726  zrhre  29842  sgnmulrp2  30383  knoppcnlem4  32125  relexpmulnn  37479  relogbmulbexp  41644
  Copyright terms: Public domain W3C validator