Metamath Proof Explorer


Syntax definition crio

Description: Extend class notation with restricted description binder.

Ref Expression
Assertion crio class ι x A | φ