Metamath Proof Explorer


Syntax definition cnx

Description: Extend class notation with the structure component index extractor.

Ref Expression
Assertion cnx class ndx