Axiom ax-1rid 6770

Description: 1 is an identity element for real multiplication. Axiom for real and complex numbers, justified by theorem ax1rid 6741. (Contributed by NM, 29-Jan-1995.)

Assertion

Ref	Expression
ax-1rid	⊢ (A ∈ ℝ → (A · 1) = A)

Detailed syntax breakdown of Axiom ax-1rid

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cr 6690	. . 3 class ℝ
3	1, 2	wcel 1390	. 2 wff A ∈ ℝ
4		c1 6692	. . . 4 class 1
5		cmul 6696	. . . 4 class ·
6	1, 4, 5	co 5455	. . 3 class (A · 1)
7	6, 1	wceq 1242	. 2 wff (A · 1) = A
8	3, 7	wi 4	1 wff (A ∈ ℝ → (A · 1) = A)

This axiom is referenced by:  mulid1  6802  mulgt1  7590  ltmulgt11  7591  lemulge11  7593  addltmul  7918