Axiom ax-1rid 7856

Description: 1 is an identity element for real multiplication. Axiom for real and complex numbers, justified by Theorem ax1rid 7814. (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 7748	. . 3 class ℝ
3	1, 2	wcel 2136	. 2 wff 𝐴 ∈ ℝ
4		c1 7750	. . . 4 class 1
5		cmul 7754	. . . 4 class ·
6	1, 4, 5	co 5841	. . 3 class (𝐴 · 1)
7	6, 1	wceq 1343	. 2 wff (𝐴 · 1) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴)

This axiom is referenced by:  mulid1  7892  mulgt1  8754  ltmulgt11  8755  lemulge11  8757  addltmul  9089