Axiom ax-1rid 11158

Description: 1 is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, justified by Theorem ax1rid 11134. Weakened from the original axiom in the form of statement in mulrid 11194, 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 11087	. . 3 class ℝ
3	1, 2	wcel 2145	. 2 wff 𝐴 ∈ ℝ
4		c1 11089	. . . 4 class 1
5		cmul 11093	. . . 4 class ·
6	1, 4, 5	co 7400	. . 3 class (𝐴 · 1)
7	6, 1	wceq 1563	. 2 wff (𝐴 · 1) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴)

This axiom is referenced by:  mulrid  11194  ltmulgt11  12065  lemulge11  12068  nnmulcl  12248  1t1e1ALT  12282  nnadddir  12283  nnmul1com  12284  addltmul  12471  xmulrid  13296  2submod  13959  cshw1  14849  sgnmulrp2  15135  bezoutlem1  16587  cshwshashnsame  17153  numclwlk1lem1  30629  numclwwlk6  30650  nmopub2tALT  32170  nmfnleub2  32187  1fldgenq  33558  unitdivcld  34208  zrhre  34326  knoppcnlem4  36947  remulcan2d  42884  sn-1ne2  42892  sn-00idlem1  43019  sn-00idlem3  43021  remul02  43026  remul01  43028  rei4  43045  remulinvcom  43054  remullid  43055  rediveq1d  43072  sn-0tie0  43085  renegmulnnass  43099  mulgt0b1d  43106  sn-ltmulgt11d  43108  sn-0lt1  43109  mulgt0b2d  43112  3cubeslem1  43277  relexpmulnn  44297  nnmul2  47922  relogbmulbexp  49192  line2xlem  49384  line2x  49385