Axiom ax-1rid 11271

Description: 1 is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, justified by Theorem ax1rid 11247. Weakened from the original axiom in the form of statement in mulrid 11307, 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 11200	. . 3 class ℝ
3	1, 2	wcel 2144	. 2 wff 𝐴 ∈ ℝ
4		c1 11202	. . . 4 class 1
5		cmul 11206	. . . 4 class ·
6	1, 4, 5	co 7420	. . 3 class (𝐴 · 1)
7	6, 1	wceq 1569	. 2 wff (𝐴 · 1) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴)

This axiom is used by:  mulrid  11307  ltmulgt11  12177  lemulge11  12180  nnmulcl  12360  1t1e1ALT  12394  nnadddir  12395  nnmul1com  12396  addltmul  12583  xmulrid  13410  2submod  14076  cshw1  14974  sgnmulrp2  15262  bezoutlem1  16713  cshwshashnsame  17282  numclwlk1lem1  30971  numclwwlk6  30992  nmopub2tALT  32512  nmfnleub2  32529  1fldgenq  33927  unitdivcld  34576  zrhre  34694  knoppcnlem4  37437  remulcan2d  43383  sn-1ne2  43406  sn-00idlem1  43525  sn-00idlem3  43527  remul02  43532  remul01  43534  rei4  43551  remulinvcom  43560  remullid  43561  rediveq1d  43578  sn-0tie0  43591  renegmulnnass  43605  mulgt0b1d  43612  sn-ltmulgt11d  43614  sn-0lt1  43615  mulgt0b2d  43618  3cubeslem1  43770  relexpmulnn  44785  nnmul2  48476  relogbmulbexp  49749  line2xlem  49941  line2x  49942