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

Definition df-oprab 6065
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 6064 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 ovmpt2 6196. (Contributed by NM, 12-Mar-1995.)
Assertion
Ref Expression
df-oprab
Distinct variable groups:   ,   ,   ,   ,

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 6062 . 2
6 vw . . . . . . . . 9
76cv 1686 . . . . . . . 8
82cv 1686 . . . . . . . . . 10
93cv 1686 . . . . . . . . . 10
108, 9cop 3856 . . . . . . . . 9
114cv 1686 . . . . . . . . 9
1210, 11cop 3856 . . . . . . . 8
137, 12wceq 1687 . . . . . . 7
1413, 1wa 362 . . . . . 6
1514, 4wex 1581 . . . . 5
1615, 3wex 1581 . . . 4
1716, 2wex 1581 . . 3
1817, 6cab 2408 . 2
195, 18wceq 1687 1
Colors of variables: wff setvar class
This definition is referenced by:  oprabid  6085  dfoprab2  6103  nfoprab1  6105  nfoprab2  6106  nfoprab3  6107  nfoprab  6108  oprabbid  6109  ssoprab2  6112  mpt20  6126  cbvoprab2  6129  eloprabga  6147  oprabrexex2  6536  eloprabi  6605  dftpos3  6725  meet0  15247  join0  15248  cnvoprab  25703  colinearex  27793
  Copyright terms: Public domain W3C validator