Axiom ax-1rid 11068

Description: 1 is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, justified by Theorem ax1rid 11044. Weakened from the original axiom in the form of statement in mulrid 11102, 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 10997	. . 3 class ℝ
3	1, 2	wcel 2110	. 2 wff 𝐴 ∈ ℝ
4		c1 10999	. . . 4 class 1
5		cmul 11003	. . . 4 class ·
6	1, 4, 5	co 7341	. . 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  11102  mulgt1OLD  11972  ltmulgt11  11973  lemulge11  11976  nnmulcl  12141  addltmul  12349  xmulrid  13170  2submod  13831  cshw1  14721  bezoutlem1  16442  cshwshashnsame  17007  numclwlk1lem1  30339  numclwwlk6  30360  nmopub2tALT  31879  nmfnleub2  31896  sgnmulrp2  32809  1fldgenq  33278  unitdivcld  33904  zrhre  34022  knoppcnlem4  36509  1t1e1ALT  42267  remulcan2d  42269  sn-1ne2  42277  nnadddir  42282  nnmul1com  42283  sn-00idlem1  42410  sn-00idlem3  42412  remul02  42417  remul01  42419  rei4  42436  remulinvcom  42445  remullid  42446  sn-0tie0  42463  renegmulnnass  42477  mulgt0b1d  42484  sn-ltmulgt11d  42486  sn-0lt1  42487  mulgt0b2d  42490  3cubeslem1  42696  relexpmulnn  43721  relogbmulbexp  48572  line2xlem  48764  line2x  48765