Axiom ax-1rid 10847

Description: 1 is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, justified by Theorem ax1rid 10823. Weakened from the original axiom in the form of statement in mulid1 10879, 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 10776	. . 3 class ℝ
3	1, 2	wcel 2112	. 2 wff 𝐴 ∈ ℝ
4		c1 10778	. . . 4 class 1
5		cmul 10782	. . . 4 class ·
6	1, 4, 5	co 7252	. . 3 class (𝐴 · 1)
7	6, 1	wceq 1543	. 2 wff (𝐴 · 1) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴)

This axiom is referenced by:  mulid1  10879  mulgt1  11739  ltmulgt11  11740  lemulge11  11742  nnmulcl  11902  addltmul  12114  xmulid1  12917  2submod  13555  cshw1  14438  bezoutlem1  16150  cshwshashnsame  16708  numclwlk1lem1  28609  numclwwlk6  28630  nmopub2tALT  30147  nmfnleub2  30164  unitdivcld  31728  zrhre  31844  sgnmulrp2  32385  knoppcnlem4  34578  1t1e1ALT  40185  remulcan2d  40186  sn-1ne2  40188  nnadddir  40193  nnmul1com  40194  sn-00idlem1  40274  sn-00idlem3  40276  remul02  40281  remul01  40283  rei4  40298  remulinvcom  40307  remulid2  40308  sn-0tie0  40314  mulgt0b2d  40323  sn-0lt1  40325  3cubeslem1  40394  relexpmulnn  41179  relogbmulbexp  45768  line2xlem  45960  line2x  45961