Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > cab  Unicode version 
Description: Introduce the class builder or class abstraction notation ("the class of sets such that is true"). Our class variables , , etc. range over class builders (implicitly in the case of defined class terms such as dfnul 3785). Note that a setvar variable can be expressed as a class builder per theorem cvjust 2451, justifying the assignment of setvar variables to class variables via the use of cv 1394. 
Ref  Expression 

wph  
vx 
Ref  Expression 

cab 
Colors of variables: wff setvar class 
Copyright terms: Public domain  W3C validator 