Metamath Proof Explorer

Axiom ax-hv0cl

Description: The zero vector is in the vector space. (Contributed by NM, 29-May-1999) (New usage is discouraged.)

Ref Expression
Assertion ax-hv0cl 0ℎ ∈ ℋ

Detailed syntax breakdown

Step Hyp Ref Expression
0 c0v ⊢ 0ℎ
1 chba ⊢ ℋ
2 0 1 wcel ⊢ 0ℎ ∈ ℋ