Axiom ax-1rid 11297

Description: 1 is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, justified by Theorem ax1rid 11273. Weakened from the original axiom in the form of statement in mulrid 11333, 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 11226	. . 3 class ℝ
3	1, 2	wcel 2147	. 2 wff 𝐴 ∈ ℝ
4		c1 11228	. . . 4 class 1
5		cmul 11232	. . . 4 class ·
6	1, 4, 5	co 7443	. . 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  11333  ltmulgt11  12203  lemulge11  12206  nnmulcl  12386  1t1e1ALT  12420  nnadddir  12421  nnmul1com  12422  addltmul  12609  xmulrid  13436  2submod  14102  cshw1  15001  sgnmulrp2  15290  bezoutlem1  16741  cshwshashnsame  17310  numclwlk1lem1  31000  numclwwlk6  31021  nmopub2tALT  32541  nmfnleub2  32558  1fldgenq  33954  unitdivcld  34603  zrhre  34721  knoppcnlem4  37540  remulcan2d  43500  sn-1ne2  43523  sn-00idlem1  43642  sn-00idlem3  43644  remul02  43649  remul01  43651  rei4  43668  remulinvcom  43677  remullid  43678  rediveq1d  43695  sn-0tie0  43708  renegmulnnass  43722  mulgt0b1d  43729  sn-ltmulgt11d  43731  sn-0lt1  43732  mulgt0b2d  43735  3cubeslem1  43887  relexpmulnn  44901  nnmul2  48605  relogbmulbexp  49878  line2xlem  50070  line2x  50071