MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cab Unicode version

Syntax Definition cab 2439
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 df-nul 3752). Note that a setvar variable can be expressed as a class builder per theorem cvjust 2448, justifying the assignment of setvar variables to class variables via the use of cv 1369.
Hypotheses
Ref Expression
wph
vx
Assertion
Ref Expression
cab

See definition df-clab 2440 for more information.

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