Axiom ax-1rid 11198

Description: 1 is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, justified by Theorem ax1rid 11174. Weakened from the original axiom in the form of statement in mulrid 11234, 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 11127	. . 3 class ℝ
3	1, 2	wcel 2145	. 2 wff 𝐴 ∈ ℝ
4		c1 11129	. . . 4 class 1
5		cmul 11133	. . . 4 class ·
6	1, 4, 5	co 7417	. . 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  11234  ltmulgt11  12102  lemulge11  12105  nnmulcl  12285  1t1e1ALT  12319  nnadddir  12320  nnmul1com  12321  addltmul  12508  xmulrid  13335  2submod  14000  cshw1  14897  sgnmulrp2  15185  bezoutlem1  16635  cshwshashnsame  17201  numclwlk1lem1  30857  numclwwlk6  30878  nmopub2tALT  32398  nmfnleub2  32415  1fldgenq  33771  unitdivcld  34419  zrhre  34537  knoppcnlem4  37201  remulcan2d  43131  sn-1ne2  43154  sn-00idlem1  43281  sn-00idlem3  43283  remul02  43288  remul01  43290  rei4  43307  remulinvcom  43316  remullid  43317  rediveq1d  43334  sn-0tie0  43347  renegmulnnass  43361  mulgt0b1d  43368  sn-ltmulgt11d  43370  sn-0lt1  43371  mulgt0b2d  43374  3cubeslem1  43537  relexpmulnn  44557  nnmul2  48226  relogbmulbexp  49499  line2xlem  49691  line2x  49692