Axiom ax-1rid 11180

Description: 1 is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, justified by Theorem ax1rid 11156. Weakened from the original axiom in the form of statement in mulrid 11212, 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 11109	. . 3 class ℝ
3	1, 2	wcel 2107	. 2 wff 𝐴 ∈ ℝ
4		c1 11111	. . . 4 class 1
5		cmul 11115	. . . 4 class ·
6	1, 4, 5	co 7409	. . 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  11212  mulgt1  12073  ltmulgt11  12074  lemulge11  12076  nnmulcl  12236  addltmul  12448  xmulrid  13258  2submod  13897  cshw1  14772  bezoutlem1  16481  cshwshashnsame  17037  numclwlk1lem1  29653  numclwwlk6  29674  nmopub2tALT  31193  nmfnleub2  31210  1fldgenq  32443  unitdivcld  32912  zrhre  33030  sgnmulrp2  33573  knoppcnlem4  35420  1t1e1ALT  41224  remulcan2d  41225  sn-1ne2  41227  nnadddir  41232  nnmul1com  41233  sn-00idlem1  41319  sn-00idlem3  41321  remul02  41326  remul01  41328  rei4  41344  remulinvcom  41353  remullid  41354  sn-0tie0  41360  renegmulnnass  41374  mulgt0b2d  41381  sn-0lt1  41383  3cubeslem1  41470  relexpmulnn  42508  relogbmulbexp  47295  line2xlem  47487  line2x  47488