Axiom ax-1rid 11176

Description: 1 is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, justified by Theorem ax1rid 11152. Weakened from the original axiom in the form of statement in mulrid 11209, 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 11105	. . 3 class ℝ
3	1, 2	wcel 2098	. 2 wff 𝐴 ∈ ℝ
4		c1 11107	. . . 4 class 1
5		cmul 11111	. . . 4 class ·
6	1, 4, 5	co 7401	. . 3 class (𝐴 · 1)
7	6, 1	wceq 1533	. 2 wff (𝐴 · 1) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴)

This axiom is referenced by:  mulrid  11209  mulgt1  12070  ltmulgt11  12071  lemulge11  12073  nnmulcl  12233  addltmul  12445  xmulrid  13255  2submod  13894  cshw1  14769  bezoutlem1  16478  cshwshashnsame  17036  numclwlk1lem1  30091  numclwwlk6  30112  nmopub2tALT  31631  nmfnleub2  31648  1fldgenq  32878  unitdivcld  33370  zrhre  33488  sgnmulrp2  34031  knoppcnlem4  35862  1t1e1ALT  41665  remulcan2d  41666  sn-1ne2  41668  nnadddir  41673  nnmul1com  41674  sn-00idlem1  41760  sn-00idlem3  41762  remul02  41767  remul01  41769  rei4  41785  remulinvcom  41794  remullid  41795  sn-0tie0  41801  renegmulnnass  41815  mulgt0b2d  41822  sn-0lt1  41824  3cubeslem1  41911  relexpmulnn  42949  relogbmulbexp  47435  line2xlem  47627  line2x  47628