Axiom ax-1rid 11145

Description: 1 is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, justified by Theorem ax1rid 11121. Weakened from the original axiom in the form of statement in mulrid 11179, 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 11074	. . 3 class ℝ
3	1, 2	wcel 2109	. 2 wff 𝐴 ∈ ℝ
4		c1 11076	. . . 4 class 1
5		cmul 11080	. . . 4 class ·
6	1, 4, 5	co 7390	. . 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  11179  mulgt1OLD  12048  ltmulgt11  12049  lemulge11  12052  nnmulcl  12217  addltmul  12425  xmulrid  13246  2submod  13904  cshw1  14794  bezoutlem1  16516  cshwshashnsame  17081  numclwlk1lem1  30305  numclwwlk6  30326  nmopub2tALT  31845  nmfnleub2  31862  sgnmulrp2  32768  1fldgenq  33279  unitdivcld  33898  zrhre  34016  knoppcnlem4  36491  1t1e1ALT  42250  remulcan2d  42252  sn-1ne2  42260  nnadddir  42265  nnmul1com  42266  sn-00idlem1  42393  sn-00idlem3  42395  remul02  42400  remul01  42402  rei4  42419  remulinvcom  42428  remullid  42429  sn-0tie0  42446  renegmulnnass  42460  mulgt0b1d  42467  sn-ltmulgt11d  42469  sn-0lt1  42470  mulgt0b2d  42473  3cubeslem1  42679  relexpmulnn  43705  relogbmulbexp  48554  line2xlem  48746  line2x  48747