Metamath Proof Explorer


Syntax definition citv

Description: Declare the syntax for the Interval (segment) index extractor.

Ref Expression
Assertion citv class Itv