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

Definition df-oprab 5528
Description: Define the class abstraction (class builder) of a collection of nested ordered pairs (for use in defining operations). This is a special case of Definition 4.16 of [TakeutiZaring] p. 14. Normally , , and are distinct, although the definition doesn't strictly require it. See df-ov 5526 for the value of an operation. The brace notation is called "class abstraction" by Quine; it is also called a "class builder" in the literature. The value of the most common operation class builder is given by ov2 in set.mm. (Contributed by SF, 5-Jan-2015.)
Assertion
Ref Expression
df-oprab
Distinct variable groups:   ,   ,   ,   ,
Allowed substitution hints:   (,,)

Detailed syntax breakdown of Definition df-oprab
StepHypRef Expression
1 wph . . 3
2 vx . . 3
3 vy . . 3
4 vz . . 3
51, 2, 3, 4coprab 5527 . 2
6 vw . . . . . . . . 9
76cv 1641 . . . . . . . 8
82cv 1641 . . . . . . . . . 10
93cv 1641 . . . . . . . . . 10
108, 9cop 4561 . . . . . . . . 9
114cv 1641 . . . . . . . . 9
1210, 11cop 4561 . . . . . . . 8
137, 12wceq 1642 . . . . . . 7
1413, 1wa 358 . . . . . 6
1514, 4wex 1541 . . . . 5
1615, 3wex 1541 . . . 4
1716, 2wex 1541 . . 3
1817, 6cab 2339 . 2
195, 18wceq 1642 1
Colors of variables: wff setvar class
This definition is referenced by:  nfoprab1  5546  nfoprab2  5547  nfoprab3  5548  nfoprab  5549  oprabid  5550  dfoprab2  5558  hboprab1  5559  hboprab2  5560  hboprab3  5561  hboprab  5562  oprabbid  5563  cbvoprab2  5568  eloprabga  5578
  Copyright terms: Public domain W3C validator