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	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 · 1 ) = 𝐴 )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1		cr	⊢ ℝ
2	0 1	wcel	⊢ 𝐴 ∈ ℝ
3		cmul	⊢ ·
4		c1	⊢ 1
5	0 4 3	co	⊢ ( 𝐴 · 1 )
6	5 0	wceq	⊢ ( 𝐴 · 1 ) = 𝐴
7	2 6	wi	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 · 1 ) = 𝐴 )