Metamath Proof Explorer

Syntax definition cab

Description: Introduce the class abstraction (or class builder) notation: { x | ph } is the class of sets x such that ph ( x ) is true. A setvar variable can be expressed as a class abstraction per Theorem cvjust , justifying the substitution of class variables for setvar variables via the use of cv .

class { x | ph }