Axiom ax-hvaddid 31163

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 31078	. . 3 class ℋ
3	1, 2	wcel 2141	. 2 wff 𝐴 ∈ ℋ
4		c0v 31083	. . . 4 class 0ℎ
5		cva 31079	. . . 4 class +ℎ
6	1, 4, 5	co 7390	. . 3 class (𝐴 +ℎ 0ℎ)
7	6, 1	wceq 1559	. 2 wff (𝐴 +ℎ 0ℎ) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℋ → (𝐴 +ℎ 0ℎ) = 𝐴)

This axiom is referenced by:  hvaddlid  31182  hvpncan  31198  hvsubeq0i  31222  hvsubcan2i  31223  hvsubaddi  31225  hvsub0  31235  hvaddsub4  31237  norm3difi  31306  shsel1  31480  shunssi  31527  omlsilem  31561  pjoc1i  31590  pjchi  31591  spansncvi  31811  5oalem1  31813  5oalem2  31814  3oalem2  31822  pjssmii  31840  hoaddridi  31945  lnop0  32125  lnopmul  32126  lnfn0i  32201  lnfnmuli  32203  pjclem4  32358  pj3si  32366  hst1h  32386  sumdmdlem  32577