Axiom ax-1rid 10607

Description: 1 is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, justified by theorem ax1rid 10583. Weakened from the original axiom in the form of statement in mulid1 10639, 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 10536	. . 3 class ℝ
3	1, 2	wcel 2114	. 2 wff 𝐴 ∈ ℝ
4		c1 10538	. . . 4 class 1
5		cmul 10542	. . . 4 class ·
6	1, 4, 5	co 7156	. . 3 class (𝐴 · 1)
7	6, 1	wceq 1537	. 2 wff (𝐴 · 1) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴)

This axiom is referenced by:  mulid1  10639  mulgt1  11499  ltmulgt11  11500  lemulge11  11502  nnmulcl  11662  addltmul  11874  xmulid1  12673  2submod  13301  cshw1  14184  bezoutlem1  15887  cshwshashnsame  16437  numclwlk1lem1  28148  numclwwlk6  28169  nmopub2tALT  29686  nmfnleub2  29703  unitdivcld  31144  zrhre  31260  sgnmulrp2  31801  knoppcnlem4  33835  1t1e1ALT  39175  remulcan2d  39176  sn-1ne2  39178  nnadddir  39183  nnmul1com  39184  sn-00idlem1  39248  sn-00idlem3  39250  remul02  39255  remul01  39257  sn-0lt1  39266  remulinvcom  39268  remulid2  39269  3cubeslem1  39301  relexpmulnn  40074  relogbmulbexp  44641  line2xlem  44760  line2x  44761