Axiom ax-1rid 11197

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

This axiom is referenced by:  mulrid  11231  mulgt1OLD  12098  ltmulgt11  12099  lemulge11  12102  nnmulcl  12262  addltmul  12475  xmulrid  13293  2submod  13948  cshw1  14838  bezoutlem1  16556  cshwshashnsame  17121  numclwlk1lem1  30296  numclwwlk6  30317  nmopub2tALT  31836  nmfnleub2  31853  sgnmulrp2  32761  1fldgenq  33262  unitdivcld  33878  zrhre  33996  knoppcnlem4  36460  1t1e1ALT  42253  remulcan2d  42255  sn-1ne2  42262  nnadddir  42267  nnmul1com  42268  sn-00idlem1  42388  sn-00idlem3  42390  remul02  42395  remul01  42397  rei4  42413  remulinvcom  42422  remullid  42423  sn-0tie0  42429  renegmulnnass  42443  mulgt0b2d  42450  sn-ltmulgt11d  42452  sn-0lt1  42453  3cubeslem1  42654  relexpmulnn  43680  relogbmulbexp  48489  line2xlem  48681  line2x  48682