Axiom ax-1rid 11138

Description: 1 is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, justified by Theorem ax1rid 11114. Weakened from the original axiom in the form of statement in mulrid 11172, 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 11067	. . 3 class ℝ
3	1, 2	wcel 2109	. 2 wff 𝐴 ∈ ℝ
4		c1 11069	. . . 4 class 1
5		cmul 11073	. . . 4 class ·
6	1, 4, 5	co 7387	. . 3 class (𝐴 · 1)
7	6, 1	wceq 1540	. 2 wff (𝐴 · 1) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴)

This axiom is referenced by:  mulrid  11172  mulgt1OLD  12041  ltmulgt11  12042  lemulge11  12045  nnmulcl  12210  addltmul  12418  xmulrid  13239  2submod  13897  cshw1  14787  bezoutlem1  16509  cshwshashnsame  17074  numclwlk1lem1  30298  numclwwlk6  30319  nmopub2tALT  31838  nmfnleub2  31855  sgnmulrp2  32761  1fldgenq  33272  unitdivcld  33891  zrhre  34009  knoppcnlem4  36484  1t1e1ALT  42243  remulcan2d  42245  sn-1ne2  42253  nnadddir  42258  nnmul1com  42259  sn-00idlem1  42386  sn-00idlem3  42388  remul02  42393  remul01  42395  rei4  42412  remulinvcom  42421  remullid  42422  sn-0tie0  42439  renegmulnnass  42453  mulgt0b1d  42460  sn-ltmulgt11d  42462  sn-0lt1  42463  mulgt0b2d  42466  3cubeslem1  42672  relexpmulnn  43698  relogbmulbexp  48550  line2xlem  48742  line2x  48743