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 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 )