Axiom ax-hvaddid 30886

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 30801	. . 3 class ℋ
3	1, 2	wcel 2098	. 2 wff 𝐴 ∈ ℋ
4		c0v 30806	. . . 4 class 0ℎ
5		cva 30802	. . . 4 class +ℎ
6	1, 4, 5	co 7419	. . 3 class (𝐴 +ℎ 0ℎ)
7	6, 1	wceq 1533	. 2 wff (𝐴 +ℎ 0ℎ) = 𝐴
8	3, 7	wi 4	1 wff (𝐴 ∈ ℋ → (𝐴 +ℎ 0ℎ) = 𝐴)

This axiom is referenced by:  hvaddlid  30905  hvpncan  30921  hvsubeq0i  30945  hvsubcan2i  30946  hvsubaddi  30948  hvsub0  30958  hvaddsub4  30960  norm3difi  31029  shsel1  31203  shunssi  31250  omlsilem  31284  pjoc1i  31313  pjchi  31314  spansncvi  31534  5oalem1  31536  5oalem2  31537  3oalem2  31545  pjssmii  31563  hoaddridi  31668  lnop0  31848  lnopmul  31849  lnfn0i  31924  lnfnmuli  31926  pjclem4  32081  pj3si  32089  hst1h  32109  sumdmdlem  32300