Metamath Proof Explorer


Syntax definition cress

Description: Extend class notation with the extensible structure builder restriction operator.

Ref Expression
Assertion cress class s