Axiom ax-1rid 11138

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

This axiom is referenced by:  mulrid  11174  mulgt1OLD  12045  ltmulgt11  12046  lemulge11  12049  nnmulcl  12229  1t1e1ALT  12263  nnadddir  12264  nnmul1com  12265  addltmul  12452  xmulrid  13277  2submod  13940  cshw1  14830  bezoutlem1  16554  cshwshashnsame  17120  numclwlk1lem1  30515  numclwwlk6  30536  nmopub2tALT  32056  nmfnleub2  32073  sgnmulrp2  32986  1fldgenq  33468  unitdivcld  34157  zrhre  34275  knoppcnlem4  36887  remulcan2d  42825  sn-1ne2  42833  sn-00idlem1  42960  sn-00idlem3  42962  remul02  42967  remul01  42969  rei4  42986  remulinvcom  42995  remullid  42996  rediveq1d  43013  sn-0tie0  43026  renegmulnnass  43040  mulgt0b1d  43047  sn-ltmulgt11d  43049  sn-0lt1  43050  mulgt0b2d  43053  3cubeslem1  43218  relexpmulnn  44238  nnmul2  47877  relogbmulbexp  49136  line2xlem  49328  line2x  49329