Axiom ax-1rid 11106

Description: 1 is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, justified by Theorem ax1rid 11082. Weakened from the original axiom in the form of statement in mulrid 11140, 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 11035	. . 3 class ℝ
3	1, 2	wcel 2119	. 2 wff 𝐴 ∈ ℝ
4		c1 11037	. . . 4 class 1
5		cmul 11041	. . . 4 class ·
6	1, 4, 5	co 7363	. . 3 class (𝐴 · 1)
7	6, 1	wceq 1547	. 2 wff (𝐴 · 1) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴)

This axiom is referenced by:  mulrid  11140  mulgt1OLD  12012  ltmulgt11  12013  lemulge11  12016  nnmulcl  12196  1t1e1ALT  12230  nnadddir  12231  nnmul1com  12232  addltmul  12411  xmulrid  13229  2submod  13892  cshw1  14782  bezoutlem1  16506  cshwshashnsame  17072  numclwlk1lem1  30464  numclwwlk6  30485  nmopub2tALT  32005  nmfnleub2  32022  sgnmulrp2  32935  1fldgenq  33413  unitdivcld  34092  zrhre  34210  knoppcnlem4  36803  remulcan2d  42741  sn-1ne2  42749  sn-00idlem1  42876  sn-00idlem3  42878  remul02  42883  remul01  42885  rei4  42902  remulinvcom  42911  remullid  42912  rediveq1d  42929  sn-0tie0  42942  renegmulnnass  42956  mulgt0b1d  42963  sn-ltmulgt11d  42965  sn-0lt1  42966  mulgt0b2d  42969  3cubeslem1  43134  relexpmulnn  44154  nnmul2  47794  relogbmulbexp  49053  line2xlem  49245  line2x  49246