Axiom ax-1rid 11242

Description: 1 is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, justified by Theorem ax1rid 11218. Weakened from the original axiom in the form of statement in mulrid 11278, 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 11171	. . 3 class ℝ
3	1, 2	wcel 2145	. 2 wff 𝐴 ∈ ℝ
4		c1 11173	. . . 4 class 1
5		cmul 11177	. . . 4 class ·
6	1, 4, 5	co 7408	. . 3 class (𝐴 · 1)
7	6, 1	wceq 1570	. 2 wff (𝐴 · 1) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴)

This axiom is used by:  mulrid  11278  ltmulgt11  12146  lemulge11  12149  nnmulcl  12329  1t1e1ALT  12363  nnadddir  12364  nnmul1com  12365  addltmul  12552  xmulrid  13379  2submod  14044  cshw1  14941  sgnmulrp2  15229  bezoutlem1  16677  cshwshashnsame  17243  numclwlk1lem1  30904  numclwwlk6  30925  nmopub2tALT  32445  nmfnleub2  32462  1fldgenq  33818  unitdivcld  34467  zrhre  34585  knoppcnlem4  37284  remulcan2d  43227  sn-1ne2  43250  sn-00idlem1  43377  sn-00idlem3  43379  remul02  43384  remul01  43386  rei4  43403  remulinvcom  43412  remullid  43413  rediveq1d  43430  sn-0tie0  43443  renegmulnnass  43457  mulgt0b1d  43464  sn-ltmulgt11d  43466  sn-0lt1  43467  mulgt0b2d  43470  3cubeslem1  43633  relexpmulnn  44653  nnmul2  48322  relogbmulbexp  49595  line2xlem  49787  line2x  49788