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

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cr 9623	. . 3 class ℝ
3	1, 2	wcel 1937	. 2 wff 𝐴 ∈ ℝ
4		c1 9625	. . . 4 class 1
5		cmul 9629	. . . 4 class ·
6	1, 4, 5	co 6363	. . 3 class (𝐴 · 1)
7	6, 1	wceq 1468	. 2 wff (𝐴 · 1) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴)

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