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 
|- 0h e. ~H

Detailed syntax breakdown

Step Hyp Ref Expression
0 c0v 
 |-  0h
1 chba 
 |-  ~H
2 0 1 wcel 
 |-  0h e. ~H