Axiom ax-1rid 11169

Description: 1 is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, justified by Theorem ax1rid 11145. Weakened from the original axiom in the form of statement in mulrid 11205, 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 11098	. . 3 class ℝ
3	1, 2	wcel 2141	. 2 wff 𝐴 ∈ ℝ
4		c1 11100	. . . 4 class 1
5		cmul 11104	. . . 4 class ·
6	1, 4, 5	co 7410	. . 3 class (𝐴 · 1)
7	6, 1	wceq 1568	. 2 wff (𝐴 · 1) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴)

This axiom is referenced by:  mulrid  11205  ltmulgt11  12073  lemulge11  12076  nnmulcl  12256  1t1e1ALT  12290  nnadddir  12291  nnmul1com  12292  addltmul  12479  xmulrid  13304  2submod  13968  cshw1  14859  sgnmulrp2  15145  bezoutlem1  16596  cshwshashnsame  17162  numclwlk1lem1  30686  numclwwlk6  30707  nmopub2tALT  32227  nmfnleub2  32244  1fldgenq  33609  unitdivcld  34257  zrhre  34375  knoppcnlem4  37051  remulcan2d  42992  sn-1ne2  43000  sn-00idlem1  43127  sn-00idlem3  43129  remul02  43134  remul01  43136  rei4  43153  remulinvcom  43162  remullid  43163  rediveq1d  43180  sn-0tie0  43193  renegmulnnass  43207  mulgt0b1d  43214  sn-ltmulgt11d  43216  sn-0lt1  43217  mulgt0b2d  43220  3cubeslem1  43385  relexpmulnn  44405  nnmul2  48034  relogbmulbexp  49308  line2xlem  49500  line2x  49501