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

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cr 9814	. . 3 class ℝ
3	1, 2	wcel 1977	. 2 wff 𝐴 ∈ ℝ
4		c1 9816	. . . 4 class 1
5		cmul 9820	. . . 4 class ·
6	1, 4, 5	co 6549	. . 3 class (𝐴 · 1)
7	6, 1	wceq 1475	. 2 wff (𝐴 · 1) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴)

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