Axiom ax-hvaddid 29375

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

Assertion

Ref	Expression
ax-hvaddid	⊢ (𝐴 ∈ ℋ → (𝐴 +ℎ 0ℎ) = 𝐴)

Detailed syntax breakdown of Axiom ax-hvaddid

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		chba 29290	. . 3 class ℋ
3	1, 2	wcel 2107	. 2 wff 𝐴 ∈ ℋ
4		c0v 29295	. . . 4 class 0ℎ
5		cva 29291	. . . 4 class +ℎ
6	1, 4, 5	co 7284	. . 3 class (𝐴 +ℎ 0ℎ)
7	6, 1	wceq 1539	. 2 wff (𝐴 +ℎ 0ℎ) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℋ → (𝐴 +ℎ 0ℎ) = 𝐴)

This axiom is referenced by:  hvaddid2  29394  hvpncan  29410  hvsubeq0i  29434  hvsubcan2i  29435  hvsubaddi  29437  hvsub0  29447  hvaddsub4  29449  norm3difi  29518  shsel1  29692  shunssi  29739  omlsilem  29773  pjoc1i  29802  pjchi  29803  spansncvi  30023  5oalem1  30025  5oalem2  30026  3oalem2  30034  pjssmii  30052  hoaddid1i  30157  lnop0  30337  lnopmul  30338  lnfn0i  30413  lnfnmuli  30415  pjclem4  30570  pj3si  30578  hst1h  30598  sumdmdlem  30789