Axiom ax-1rid 11097

Description: 1 is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, justified by Theorem ax1rid 11073. Weakened from the original axiom in the form of statement in mulrid 11131, 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 11026	. . 3 class ℝ
3	1, 2	wcel 2114	. 2 wff 𝐴 ∈ ℝ
4		c1 11028	. . . 4 class 1
5		cmul 11032	. . . 4 class ·
6	1, 4, 5	co 7358	. . 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  11131  mulgt1OLD  12001  ltmulgt11  12002  lemulge11  12005  nnmulcl  12170  addltmul  12378  xmulrid  13195  2submod  13856  cshw1  14746  bezoutlem1  16467  cshwshashnsame  17032  numclwlk1lem1  30428  numclwwlk6  30449  nmopub2tALT  31969  nmfnleub2  31986  sgnmulrp2  32900  1fldgenq  33388  unitdivcld  34051  zrhre  34169  knoppcnlem4  36754  1t1e1ALT  42686  remulcan2d  42688  sn-1ne2  42696  nnadddir  42701  nnmul1com  42702  sn-00idlem1  42829  sn-00idlem3  42831  remul02  42836  remul01  42838  rei4  42855  remulinvcom  42864  remullid  42865  rediveq1d  42882  sn-0tie0  42895  renegmulnnass  42909  mulgt0b1d  42916  sn-ltmulgt11d  42918  sn-0lt1  42919  mulgt0b2d  42922  3cubeslem1  43115  relexpmulnn  44139  relogbmulbexp  48995  line2xlem  49187  line2x  49188