Metamath Proof Explorer


Syntax definition wl-crab

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

Ref Expression
Assertion wl-crab class x : A | φ