NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  cab Unicode version

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

See definition df-clab 2340 for more information.

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