Axiom ax-1rid 7860

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

Assertion

Ref	Expression
ax-1rid	|- ( A e. RR -> ( A x. 1 ) = A )

Detailed syntax breakdown of Axiom ax-1rid

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cr 7752	. . 3 class RR
3	1, 2	wcel 2136	. 2 wff A e. RR
4		c1 7754	. . . 4 class 1
5		cmul 7758	. . . 4 class x.
6	1, 4, 5	co 5842	. . 3 class ( A x. 1 )
7	6, 1	wceq 1343	. 2 wff ( A x. 1 ) = A
8	3, 7	wi 4	1 wff ( A e. RR -> ( A x. 1 ) = A )

This axiom is referenced by:  mulid1  7896  mulgt1  8758  ltmulgt11  8759  lemulge11  8761  addltmul  9093