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

Definition df-oprab 6300
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 6299 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 6438. (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 6297 . 2
6 vw . . . . . . . . 9
76cv 1394 . . . . . . . 8
82cv 1394 . . . . . . . . . 10
93cv 1394 . . . . . . . . . 10
108, 9cop 4035 . . . . . . . . 9
114cv 1394 . . . . . . . . 9
1210, 11cop 4035 . . . . . . . 8
137, 12wceq 1395 . . . . . . 7
1413, 1wa 369 . . . . . 6
1514, 4wex 1612 . . . . 5
1615, 3wex 1612 . . . 4
1716, 2wex 1612 . . 3
1817, 6cab 2442 . 2
195, 18wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  oprabid  6323  dfoprab2  6343  nfoprab1  6346  nfoprab2  6347  nfoprab3  6348  nfoprab  6349  oprabbid  6350  ssoprab2  6353  mpt20  6367  cbvoprab2  6370  eloprabga  6389  oprabrexex2  6790  eloprabi  6862  dftpos3  6992  meet0  15767  join0  15768  cnvoprab  27546  mppspstlem  28931  mppsval  28932  colinearex  29710
  Copyright terms: Public domain W3C validator