Axiom ax-1rid 10596

Description: 1 is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, justified by theorem ax1rid 10572. Weakened from the original axiom in the form of statement in mulid1 10628, 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 10525	. . 3 class ℝ
3	1, 2	wcel 2111	. 2 wff 𝐴 ∈ ℝ
4		c1 10527	. . . 4 class 1
5		cmul 10531	. . . 4 class ·
6	1, 4, 5	co 7135	. . 3 class (𝐴 · 1)
7	6, 1	wceq 1538	. 2 wff (𝐴 · 1) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴)

This axiom is referenced by:  mulid1  10628  mulgt1  11488  ltmulgt11  11489  lemulge11  11491  nnmulcl  11649  addltmul  11861  xmulid1  12660  2submod  13295  cshw1  14175  bezoutlem1  15877  cshwshashnsame  16429  numclwlk1lem1  28154  numclwwlk6  28175  nmopub2tALT  29692  nmfnleub2  29709  unitdivcld  31254  zrhre  31370  sgnmulrp2  31911  knoppcnlem4  33948  1t1e1ALT  39463  remulcan2d  39464  sn-1ne2  39466  nnadddir  39471  nnmul1com  39472  sn-00idlem1  39536  sn-00idlem3  39538  remul02  39543  remul01  39545  rei4  39560  remulinvcom  39569  remulid2  39570  sn-0tie0  39576  mulgt0b2d  39585  sn-0lt1  39587  3cubeslem1  39625  relexpmulnn  40410  relogbmulbexp  44975  line2xlem  45167  line2x  45168