Metamath Proof Explorer


Syntax definition crio

Description: Extend class notation with restricted description binder.

Ref Expression
Assertion crio class ( 𝑥𝐴 𝜑 )