This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$class A$
1		cr	$class ℝ$
2	0 1	wcel	$wff A \in ℝ$
3		cmul	$class \times$
4		c1	$class 1$
5	0 4 3	co	$class A \cdot 1$
6	5 0	wceq	$wff A \cdot 1 = A$
7	2 6	wi	$wff (A \in ℝ \to A \cdot 1 = A)$