Axiom ax-1rid 11108

Description: 1 is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, justified by Theorem ax1rid 11084. Weakened from the original axiom in the form of statement in mulrid 11142, 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 11037	. . 3 class ℝ
3	1, 2	wcel 2114	. 2 wff 𝐴 ∈ ℝ
4		c1 11039	. . . 4 class 1
5		cmul 11043	. . . 4 class ·
6	1, 4, 5	co 7367	. . 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  11142  mulgt1OLD  12014  ltmulgt11  12015  lemulge11  12018  nnmulcl  12198  1t1e1ALT  12232  nnadddir  12233  nnmul1com  12234  addltmul  12413  xmulrid  13231  2submod  13894  cshw1  14784  bezoutlem1  16508  cshwshashnsame  17074  numclwlk1lem1  30439  numclwwlk6  30460  nmopub2tALT  31980  nmfnleub2  31997  sgnmulrp2  32909  1fldgenq  33383  unitdivcld  34045  zrhre  34163  knoppcnlem4  36756  remulcan2d  42695  sn-1ne2  42703  sn-00idlem1  42830  sn-00idlem3  42832  remul02  42837  remul01  42839  rei4  42856  remulinvcom  42865  remullid  42866  rediveq1d  42883  sn-0tie0  42896  renegmulnnass  42910  mulgt0b1d  42917  sn-ltmulgt11d  42919  sn-0lt1  42920  mulgt0b2d  42923  3cubeslem1  43116  relexpmulnn  44136  nnmul2  47772  relogbmulbexp  49031  line2xlem  49223  line2x  49224