Axiom ax-1rid 11130

Description: 1 is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, justified by Theorem ax1rid 11106. Weakened from the original axiom in the form of statement in mulrid 11162, 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 11059	. . 3 class ℝ
3	1, 2	wcel 2106	. 2 wff 𝐴 ∈ ℝ
4		c1 11061	. . . 4 class 1
5		cmul 11065	. . . 4 class ·
6	1, 4, 5	co 7362	. . 3 class (𝐴 · 1)
7	6, 1	wceq 1541	. 2 wff (𝐴 · 1) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴)

This axiom is referenced by:  mulrid  11162  mulgt1  12023  ltmulgt11  12024  lemulge11  12026  nnmulcl  12186  addltmul  12398  xmulrid  13208  2submod  13847  cshw1  14722  bezoutlem1  16431  cshwshashnsame  16987  numclwlk1lem1  29376  numclwwlk6  29397  nmopub2tALT  30914  nmfnleub2  30931  1fldgenq  32160  unitdivcld  32571  zrhre  32689  sgnmulrp2  33232  knoppcnlem4  35035  1t1e1ALT  40836  remulcan2d  40837  sn-1ne2  40839  nnadddir  40844  nnmul1com  40845  sn-00idlem1  40925  sn-00idlem3  40927  remul02  40932  remul01  40934  rei4  40950  remulinvcom  40959  remullid  40960  sn-0tie0  40966  renegmulnnass  40980  mulgt0b2d  40987  sn-0lt1  40989  3cubeslem1  41065  relexpmulnn  42103  relogbmulbexp  46767  line2xlem  46959  line2x  46960