Metamath Proof Explorer


Syntax definition crio

Description: Extend class notation with restricted description binder.

Ref Expression
Assertion crio class ι x ∈ A | φ