Metamath Proof Explorer


Syntax definition cdveca

Description: Extend class notation with constructed vector space A.

Ref Expression
Assertion cdveca class DVecA