Axiom ax-1rid 10169

Description: 1 is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, justified by theorem ax1rid 10145. Weakened from the original axiom in the form of statement in mulid1 10200, 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 10098	. . 3 class ℝ
3	1, 2	wcel 2127	. 2 wff 𝐴 ∈ ℝ
4		c1 10100	. . . 4 class 1
5		cmul 10104	. . . 4 class ·
6	1, 4, 5	co 6801	. . 3 class (𝐴 · 1)
7	6, 1	wceq 1620	. 2 wff (𝐴 · 1) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴)

This axiom is referenced by:  mulid1  10200  mulgt1  11045  ltmulgt11  11046  lemulge11  11048  addltmul  11431  xmulid1  12273  2submod  12896  cshw1  13739  bezoutlem1  15429  cshwshashnsame  15983  numclwlk1lem1  27501  numclwwlk6  27529  nmopub2tALT  29048  nmfnleub2  29065  unitdivcld  30227  zrhre  30343  sgnmulrp2  30885  knoppcnlem4  32763  relexpmulnn  38472  relogbmulbexp  42834