Axiom ax-1rid 11100

Description: 1 is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, justified by Theorem ax1rid 11076. Weakened from the original axiom in the form of statement in mulrid 11134, 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 11029	. . 3 class ℝ
3	1, 2	wcel 2114	. 2 wff 𝐴 ∈ ℝ
4		c1 11031	. . . 4 class 1
5		cmul 11035	. . . 4 class ·
6	1, 4, 5	co 7360	. . 3 class (𝐴 · 1)
7	6, 1	wceq 1542	. 2 wff (𝐴 · 1) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴)

This axiom is referenced by:  mulrid  11134  mulgt1OLD  12004  ltmulgt11  12005  lemulge11  12008  nnmulcl  12173  addltmul  12381  xmulrid  13198  2submod  13859  cshw1  14749  bezoutlem1  16470  cshwshashnsame  17035  numclwlk1lem1  30427  numclwwlk6  30448  nmopub2tALT  31967  nmfnleub2  31984  sgnmulrp2  32898  1fldgenq  33385  unitdivcld  34039  zrhre  34157  knoppcnlem4  36671  1t1e1ALT  42546  remulcan2d  42548  sn-1ne2  42556  nnadddir  42561  nnmul1com  42562  sn-00idlem1  42689  sn-00idlem3  42691  remul02  42696  remul01  42698  rei4  42715  remulinvcom  42724  remullid  42725  sn-0tie0  42742  renegmulnnass  42756  mulgt0b1d  42763  sn-ltmulgt11d  42765  sn-0lt1  42766  mulgt0b2d  42769  3cubeslem1  42962  relexpmulnn  43986  relogbmulbexp  48843  line2xlem  49035  line2x  49036