Axiom ax-1rid 11222

Description: 1 is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, justified by Theorem ax1rid 11198. Weakened from the original axiom in the form of statement in mulrid 11256, 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 11151	. . 3 class ℝ
3	1, 2	wcel 2105	. 2 wff 𝐴 ∈ ℝ
4		c1 11153	. . . 4 class 1
5		cmul 11157	. . . 4 class ·
6	1, 4, 5	co 7430	. . 3 class (𝐴 · 1)
7	6, 1	wceq 1536	. 2 wff (𝐴 · 1) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴)

This axiom is referenced by:  mulrid  11256  mulgt1OLD  12123  ltmulgt11  12124  lemulge11  12127  nnmulcl  12287  addltmul  12499  xmulrid  13317  2submod  13969  cshw1  14856  bezoutlem1  16572  cshwshashnsame  17137  numclwlk1lem1  30397  numclwwlk6  30418  nmopub2tALT  31937  nmfnleub2  31954  1fldgenq  33303  unitdivcld  33861  zrhre  33981  sgnmulrp2  34524  knoppcnlem4  36478  1t1e1ALT  42274  remulcan2d  42276  sn-1ne2  42278  nnadddir  42283  nnmul1com  42284  sn-00idlem1  42404  sn-00idlem3  42406  remul02  42411  remul01  42413  rei4  42429  remulinvcom  42438  remullid  42439  sn-0tie0  42445  renegmulnnass  42459  mulgt0b2d  42466  sn-ltmulgt11d  42468  sn-0lt1  42469  3cubeslem1  42671  relexpmulnn  43698  relogbmulbexp  48410  line2xlem  48602  line2x  48603