Metamath Proof Explorer


Syntax definition crio

Description: Extend class notation with restricted description binder.

Ref Expression
Assertion crio
class ( iota_ x e. A ph )