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 .

Ref Expression
Assertion cab class { 𝑥𝜑 }