Metamath Proof Explorer


Syntax definition crab

Description: Extend class notation to include the restricted class abstraction (class builder).

Ref Expression
Assertion crab class { 𝑥𝐴𝜑 }