Axiom ax-hvaddid 4988

Description: Addition with the zero vector.

Assertion

Ref	Expression
ax-hvaddid	⊢ (A ∈ ℋ → (A +v 0v) = A)

Detailed syntax breakdown of Axiom ax-hvaddid

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		chil 4958	. . 3 class ℋ
3	1, 2	wcel 1092	. 2 wff A ∈ ℋ
4		c0v 4961	. . . 4 class 0v
5		cva 4959	. . . 4 class +v
6	1, 4, 5	co 3001	. . 3 class (A +v 0v)
7	6, 1	wceq 1091	. 2 wff (A +v 0v) = A
8	3, 7	wi 2	1 wff (A ∈ ℋ → (A +v 0v) = A)

This axiom is referenced by:  hvaddid2t 5003  hvsubcan1t 5016  hvsubeq0 5035  hvsubcan2 5036  hvsubadd 5038  hvsub0t 5041  norm3dif 5094  chocuni 5179  pjthlem14 5238  omlsilem 5249  pjoc1 5268  pjch 5269  shsel1t 5286  shunss 5338  spansncv 5542  5oalem1 5544  5oalem2 5545  3oalem2 5553  pjssm 5572  pjv 5589  hoid0 5614  pjclem4 5653  pj3s 5659  sumdmdlem 5786

metamath.org