Axiom ax-1rid 11108

Description: 1 is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, justified by Theorem ax1rid 11084. Weakened from the original axiom in the form of statement in mulrid 11142, 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 11037	. . 3 class ℝ
3	1, 2	wcel 2114	. 2 wff 𝐴 ∈ ℝ
4		c1 11039	. . . 4 class 1
5		cmul 11043	. . . 4 class ·
6	1, 4, 5	co 7368	. . 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  11142  mulgt1OLD  12012  ltmulgt11  12013  lemulge11  12016  nnmulcl  12181  addltmul  12389  xmulrid  13206  2submod  13867  cshw1  14757  bezoutlem1  16478  cshwshashnsame  17043  numclwlk1lem1  30456  numclwwlk6  30477  nmopub2tALT  31996  nmfnleub2  32013  sgnmulrp2  32927  1fldgenq  33415  unitdivcld  34078  zrhre  34196  knoppcnlem4  36715  1t1e1ALT  42614  remulcan2d  42616  sn-1ne2  42624  nnadddir  42629  nnmul1com  42630  sn-00idlem1  42757  sn-00idlem3  42759  remul02  42764  remul01  42766  rei4  42783  remulinvcom  42792  remullid  42793  sn-0tie0  42810  renegmulnnass  42824  mulgt0b1d  42831  sn-ltmulgt11d  42833  sn-0lt1  42834  mulgt0b2d  42837  3cubeslem1  43030  relexpmulnn  44054  relogbmulbexp  48910  line2xlem  49102  line2x  49103