Axiom ax-1rid

Description: 1 is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, justified by Theorem ax1rid . Weakened from the original axiom in the form of statement in mulid1 , based on ideas by Eric Schmidt. (Contributed by NM, 29-Jan-1995)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	|- A
1		cr	|- RR
2	0 1	wcel	|- A e. RR
3		cmul	|- x.
4		c1	|- 1
5	0 4 3	co	|- ( A x. 1 )
6	5 0	wceq	|- ( A x. 1 ) = A
7	2 6	wi	|- ( A e. RR -> ( A x. 1 ) = A )