Axiom ax-1rid 11188

Description: 1 is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, justified by Theorem ax1rid 11164. Weakened from the original axiom in the form of statement in mulrid 11224, 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 11117	. . 3 class ℝ
3	1, 2	wcel 2146	. 2 wff 𝐴 ∈ ℝ
4		c1 11119	. . . 4 class 1
5		cmul 11123	. . . 4 class ·
6	1, 4, 5	co 7423	. . 3 class (𝐴 · 1)
7	6, 1	wceq 1570	. 2 wff (𝐴 · 1) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴)

This axiom is used by:  mulrid  11224  ltmulgt11  12092  lemulge11  12095  nnmulcl  12275  1t1e1ALT  12309  nnadddir  12310  nnmul1com  12311  addltmul  12498  xmulrid  13323  2submod  13988  cshw1  14885  sgnmulrp2  15171  bezoutlem1  16622  cshwshashnsame  17188  numclwlk1lem1  30750  numclwwlk6  30771  nmopub2tALT  32291  nmfnleub2  32308  1fldgenq  33667  unitdivcld  34315  zrhre  34433  knoppcnlem4  37118  remulcan2d  43057  sn-1ne2  43065  sn-00idlem1  43192  sn-00idlem3  43194  remul02  43199  remul01  43201  rei4  43218  remulinvcom  43227  remullid  43228  rediveq1d  43245  sn-0tie0  43258  renegmulnnass  43272  mulgt0b1d  43279  sn-ltmulgt11d  43281  sn-0lt1  43282  mulgt0b2d  43285  3cubeslem1  43448  relexpmulnn  44468  nnmul2  48100  relogbmulbexp  49374  line2xlem  49566  line2x  49567