Axiom ax-1rid 11086

Description: 1 is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, justified by Theorem ax1rid 11062. Weakened from the original axiom in the form of statement in mulrid 11120, 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 11015	. . 3 class ℝ
3	1, 2	wcel 2113	. 2 wff 𝐴 ∈ ℝ
4		c1 11017	. . . 4 class 1
5		cmul 11021	. . . 4 class ·
6	1, 4, 5	co 7355	. . 3 class (𝐴 · 1)
7	6, 1	wceq 1541	. 2 wff (𝐴 · 1) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴)

This axiom is referenced by:  mulrid  11120  mulgt1OLD  11990  ltmulgt11  11991  lemulge11  11994  nnmulcl  12159  addltmul  12367  xmulrid  13188  2submod  13849  cshw1  14739  bezoutlem1  16460  cshwshashnsame  17025  numclwlk1lem1  30360  numclwwlk6  30381  nmopub2tALT  31900  nmfnleub2  31917  sgnmulrp2  32830  1fldgenq  33299  unitdivcld  33925  zrhre  34043  knoppcnlem4  36551  1t1e1ALT  42363  remulcan2d  42365  sn-1ne2  42373  nnadddir  42378  nnmul1com  42379  sn-00idlem1  42506  sn-00idlem3  42508  remul02  42513  remul01  42515  rei4  42532  remulinvcom  42541  remullid  42542  sn-0tie0  42559  renegmulnnass  42573  mulgt0b1d  42580  sn-ltmulgt11d  42582  sn-0lt1  42583  mulgt0b2d  42586  3cubeslem1  42791  relexpmulnn  43816  relogbmulbexp  48676  line2xlem  48868  line2x  48869