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 mulrid , based on ideas by Eric Schmidt. (Contributed by NM, 29-Jan-1995)

	Ref	Expression
Assertion	ax-1rid	$$⊢A\in ℝ\to A\cdot 1=A$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1		cr	$$classℝ$$
2	0 1	wcel	$$wffA\in ℝ$$
3		cmul	$$class\times$$
4		c1	$$class1$$
5	0 4 3	co	$$classA\cdot 1$$
6	5 0	wceq	$$wffA\cdot 1=A$$
7	2 6	wi	$$wff\left(A\in ℝ\to A\cdot 1=A\right)$$