Axiom ax-1rid 10607

Description: 1 is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, justified by theorem ax1rid 10583. Weakened from the original axiom in the form of statement in mulid1 10639, 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 10536	. . 3 class ℝ
3	1, 2	wcel 2114	. 2 wff 𝐴 ∈ ℝ
4		c1 10538	. . . 4 class 1
5		cmul 10542	. . . 4 class ·
6	1, 4, 5	co 7156	. . 3 class (𝐴 · 1)
7	6, 1	wceq 1537	. 2 wff (𝐴 · 1) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴)

This axiom is referenced by:  mulid1  10639  mulgt1  11499  ltmulgt11  11500  lemulge11  11502  nnmulcl  11662  addltmul  11874  xmulid1  12673  2submod  13301  cshw1  14184  bezoutlem1  15887  cshwshashnsame  16437  numclwlk1lem1  28148  numclwwlk6  28169  nmopub2tALT  29686  nmfnleub2  29703  unitdivcld  31144  zrhre  31260  sgnmulrp2  31801  knoppcnlem4  33835  1t1e1ALT  39204  remulcan2d  39205  sn-1ne2  39207  nnadddir  39212  nnmul1com  39213  sn-00idlem1  39277  sn-00idlem3  39279  remul02  39284  remul01  39286  sn-0lt1  39295  remulinvcom  39297  remulid2  39298  3cubeslem1  39330  relexpmulnn  40103  relogbmulbexp  44670  line2xlem  44789  line2x  44790