Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > cab  Structured version 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 3629). Note that a set variable can be expressed as a class builder per theorem cvjust 2431, justifying the assignment of set variables to class variables via the use of cv 1651. 
Ref  Expression 

wph  
vx 
Ref  Expression 

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