Axiom ax-hvmulid

Description: Scalar multiplication by one. (Contributed by NM, 30-May-1999) (New usage is discouraged.)

	Ref	Expression
Assertion	ax-hvmulid	$$⊢A\in \mathscr{H}\to 1{\cdot }_{ℎ}A=A$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1		chba	$$class\mathscr{H}$$
2	0 1	wcel	$$wffA\in \mathscr{H}$$
3		c1	$$class1$$
4		csm	$$class{\cdot }_{ℎ}$$
5	3 0 4	co	$$class\left(1{\cdot }_{ℎ}A\right)$$
6	5 0	wceq	$$wff1{\cdot }_{ℎ}A=A$$
7	2 6	wi	$$wff\left(A\in \mathscr{H}\to 1{\cdot }_{ℎ}A=A\right)$$