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

Syntax Definition cab 2023
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 2032, justifying the assignment of setvar variables to class variables via the use of cv 1241.
Hypotheses
Ref Expression
wph
vx  setvar
Assertion
Ref Expression
cab  {  |  }

See definition df-clab 2024 for more information.

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