Axiom ax-1rid 11254

Description: 1 is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, justified by Theorem ax1rid 11230. Weakened from the original axiom in the form of statement in mulrid 11288, 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 11183	. . 3 class ℝ
3	1, 2	wcel 2108	. 2 wff 𝐴 ∈ ℝ
4		c1 11185	. . . 4 class 1
5		cmul 11189	. . . 4 class ·
6	1, 4, 5	co 7448	. . 3 class (𝐴 · 1)
7	6, 1	wceq 1537	. 2 wff (𝐴 · 1) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴)

This axiom is referenced by:  mulrid  11288  mulgt1OLD  12153  ltmulgt11  12154  lemulge11  12157  nnmulcl  12317  addltmul  12529  xmulrid  13341  2submod  13983  cshw1  14870  bezoutlem1  16586  cshwshashnsame  17151  numclwlk1lem1  30401  numclwwlk6  30422  nmopub2tALT  31941  nmfnleub2  31958  1fldgenq  33289  unitdivcld  33847  zrhre  33965  sgnmulrp2  34508  knoppcnlem4  36462  1t1e1ALT  42250  remulcan2d  42252  sn-1ne2  42254  nnadddir  42259  nnmul1com  42260  sn-00idlem1  42374  sn-00idlem3  42376  remul02  42381  remul01  42383  rei4  42399  remulinvcom  42408  remullid  42409  sn-0tie0  42415  renegmulnnass  42429  mulgt0b2d  42436  sn-ltmulgt11d  42438  sn-0lt1  42439  3cubeslem1  42640  relexpmulnn  43671  relogbmulbexp  48295  line2xlem  48487  line2x  48488