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 mulid1 , 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 ) = 𝐴 )