Metamath Proof Explorer


Syntax definition crio

Description: Extend class notation with restricted description binder.

Ref Expression
Assertion crio class ( ℩ 𝑥 ∈ 𝐴 𝜑 )