Axiom ax-hvaddid 29374

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 29289	. . 3 class ℋ
3	1, 2	wcel 2106	. 2 wff 𝐴 ∈ ℋ
4		c0v 29294	. . . 4 class 0ℎ
5		cva 29290	. . . 4 class +ℎ
6	1, 4, 5	co 7267	. . 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  29393  hvpncan  29409  hvsubeq0i  29433  hvsubcan2i  29434  hvsubaddi  29436  hvsub0  29446  hvaddsub4  29448  norm3difi  29517  shsel1  29691  shunssi  29738  omlsilem  29772  pjoc1i  29801  pjchi  29802  spansncvi  30022  5oalem1  30024  5oalem2  30025  3oalem2  30033  pjssmii  30051  hoaddid1i  30156  lnop0  30336  lnopmul  30337  lnfn0i  30412  lnfnmuli  30414  pjclem4  30569  pj3si  30577  hst1h  30597  sumdmdlem  30788