Axiom ax-hvaddid

Description: Addition with the zero vector. (Contributed by NM, 16-Aug-1999) (New usage is discouraged.)

	Ref	Expression
Assertion	ax-hvaddid	$$⊢A\in \mathscr{H}\to A{+}_{ℎ}{0}_{ℎ}=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		cva	$$class{+}_{ℎ}$$
4		c0v	$$class{0}_{ℎ}$$
5	0 4 3	co	$$class\left(A{+}_{ℎ}{0}_{ℎ}\right)$$
6	5 0	wceq	$$wffA{+}_{ℎ}{0}_{ℎ}=A$$
7	2 6	wi	$$wff\left(A\in \mathscr{H}\to A{+}_{ℎ}{0}_{ℎ}=A\right)$$