Syntax Definition c0v 4961

Description: Extend class notation with zero vector in Hilbert space.

Assertion

Ref	Expression
c0v	class 0v

This syntax is primitive. The first axiom using it is ax-hvzercl 4987.

metamath.org