Axiom ax-1rid 11098

Description: 1 is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, justified by Theorem ax1rid 11074. Weakened from the original axiom in the form of statement in mulrid 11132, 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 11027	. . 3 class ℝ
3	1, 2	wcel 2109	. 2 wff 𝐴 ∈ ℝ
4		c1 11029	. . . 4 class 1
5		cmul 11033	. . . 4 class ·
6	1, 4, 5	co 7353	. . 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  11132  mulgt1OLD  12001  ltmulgt11  12002  lemulge11  12005  nnmulcl  12170  addltmul  12378  xmulrid  13199  2submod  13857  cshw1  14746  bezoutlem1  16468  cshwshashnsame  17033  numclwlk1lem1  30331  numclwwlk6  30352  nmopub2tALT  31871  nmfnleub2  31888  sgnmulrp2  32794  1fldgenq  33271  unitdivcld  33867  zrhre  33985  knoppcnlem4  36469  1t1e1ALT  42228  remulcan2d  42230  sn-1ne2  42238  nnadddir  42243  nnmul1com  42244  sn-00idlem1  42371  sn-00idlem3  42373  remul02  42378  remul01  42380  rei4  42397  remulinvcom  42406  remullid  42407  sn-0tie0  42424  renegmulnnass  42438  mulgt0b1d  42445  sn-ltmulgt11d  42447  sn-0lt1  42448  mulgt0b2d  42451  3cubeslem1  42657  relexpmulnn  43682  relogbmulbexp  48534  line2xlem  48726  line2x  48727