Axiom ax-1rid 11097

Description: 1 is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, justified by Theorem ax1rid 11073. Weakened from the original axiom in the form of statement in mulrid 11131, 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 11026	. . 3 class ℝ
3	1, 2	wcel 2114	. 2 wff 𝐴 ∈ ℝ
4		c1 11028	. . . 4 class 1
5		cmul 11032	. . . 4 class ·
6	1, 4, 5	co 7358	. . 3 class (𝐴 · 1)
7	6, 1	wceq 1542	. 2 wff (𝐴 · 1) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴)

This axiom is referenced by:  mulrid  11131  mulgt1OLD  12003  ltmulgt11  12004  lemulge11  12007  nnmulcl  12187  1t1e1ALT  12221  nnadddir  12222  nnmul1com  12223  addltmul  12402  xmulrid  13220  2submod  13883  cshw1  14773  bezoutlem1  16497  cshwshashnsame  17063  numclwlk1lem1  30459  numclwwlk6  30480  nmopub2tALT  32000  nmfnleub2  32017  sgnmulrp2  32929  1fldgenq  33403  unitdivcld  34066  zrhre  34184  knoppcnlem4  36769  remulcan2d  42706  sn-1ne2  42714  sn-00idlem1  42841  sn-00idlem3  42843  remul02  42848  remul01  42850  rei4  42867  remulinvcom  42876  remullid  42877  rediveq1d  42894  sn-0tie0  42907  renegmulnnass  42921  mulgt0b1d  42928  sn-ltmulgt11d  42930  sn-0lt1  42931  mulgt0b2d  42934  3cubeslem1  43127  relexpmulnn  44151  nnmul2  47775  relogbmulbexp  49034  line2xlem  49226  line2x  49227