Axiom ax-1rid 10006

Description: 1 is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, justified by theorem ax1rid 9982. Weakened from the original axiom in the form of statement in mulid1 10037, 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 9935	. . 3 class ℝ
3	1, 2	wcel 1990	. 2 wff 𝐴 ∈ ℝ
4		c1 9937	. . . 4 class 1
5		cmul 9941	. . . 4 class ·
6	1, 4, 5	co 6650	. . 3 class (𝐴 · 1)
7	6, 1	wceq 1483	. 2 wff (𝐴 · 1) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴)

This axiom is referenced by:  mulid1  10037  mulgt1  10882  ltmulgt11  10883  lemulge11  10885  addltmul  11268  xmulid1  12109  2submod  12731  cshw1  13568  bezoutlem1  15256  cshwshashnsame  15810  numclwwlk6  27248  nmopub2tALT  28768  nmfnleub2  28785  unitdivcld  29947  zrhre  30063  sgnmulrp2  30605  knoppcnlem4  32486  relexpmulnn  38001  relogbmulbexp  42355