Axiom ax-1rid 11225

Description: 1 is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, justified by Theorem ax1rid 11201. Weakened from the original axiom in the form of statement in mulrid 11259, 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 11154	. . 3 class ℝ
3	1, 2	wcel 2108	. 2 wff 𝐴 ∈ ℝ
4		c1 11156	. . . 4 class 1
5		cmul 11160	. . . 4 class ·
6	1, 4, 5	co 7431	. . 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  11259  mulgt1OLD  12126  ltmulgt11  12127  lemulge11  12130  nnmulcl  12290  addltmul  12502  xmulrid  13321  2submod  13973  cshw1  14860  bezoutlem1  16576  cshwshashnsame  17141  numclwlk1lem1  30388  numclwwlk6  30409  nmopub2tALT  31928  nmfnleub2  31945  1fldgenq  33324  unitdivcld  33900  zrhre  34020  sgnmulrp2  34546  knoppcnlem4  36497  1t1e1ALT  42296  remulcan2d  42298  sn-1ne2  42300  nnadddir  42305  nnmul1com  42306  sn-00idlem1  42428  sn-00idlem3  42430  remul02  42435  remul01  42437  rei4  42453  remulinvcom  42462  remullid  42463  sn-0tie0  42469  renegmulnnass  42483  mulgt0b2d  42490  sn-ltmulgt11d  42492  sn-0lt1  42493  3cubeslem1  42695  relexpmulnn  43722  relogbmulbexp  48482  line2xlem  48674  line2x  48675