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 10322
Description: 1 is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, justified by theorem ax1rid 10298. Weakened from the original axiom in the form of statement in mulid1 10354, 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 10251 . . 3 class
31, 2wcel 2164 . 2 wff 𝐴 ∈ ℝ
4 c1 10253 . . . 4 class 1
5 cmul 10257 . . . 4 class ·
61, 4, 5co 6905 . . 3 class (𝐴 · 1)
76, 1wceq 1656 . 2 wff (𝐴 · 1) = 𝐴
83, 7wi 4 1 wff (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴)
Colors of variables: wff setvar class
This axiom is referenced by:  mulid1  10354  mulgt1  11212  ltmulgt11  11213  lemulge11  11215  nnmulcl  11375  addltmul  11594  xmulid1  12397  2submod  13026  cshw1  13943  bezoutlem1  15629  cshwshashnsame  16176  numclwlk1lem1  27761  numclwwlk6  27794  nmopub2tALT  29312  nmfnleub2  29329  unitdivcld  30481  zrhre  30597  sgnmulrp2  31140  knoppcnlem4  33008  1t1e1ALT  38045  relexpmulnn  38835  relogbmulbexp  43195  line2xlem  43298  line2x  43299
  Copyright terms: Public domain W3C validator