ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  cab Structured version   Unicode version

Syntax Definition cab 2004
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 (sometimes implicitly). Note that a setvar variable can be expressed as a class builder per theorem cvjust 2013, justifying the assignment of setvar variables to class variables via the use of cv 1225.
Hypotheses
Ref Expression
wph
vx  setvar
Assertion
Ref Expression
cab  {  |  }

See definition df-clab 2005 for more information.

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