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

Definition df-opab 4511
Description: Define the class abstraction of a collection of ordered pairs. Definition 3.3 of [Monk1] p. 34. Usually and are distinct, although the definition doesn't strictly require it (see dfid2 4802 for a case where they are not distinct). The brace notation is called "class abstraction" by Quine; it is also (more commonly) called a "class builder" in the literature. An alternate definition using no existential quantifiers is shown by dfopab2 6854. For example, ->3 4 (ex-opab 25153). (Contributed by NM, 4-Jul-1994.)
Assertion
Ref Expression
df-opab
Distinct variable groups:   ,   ,   ,

Detailed syntax breakdown of Definition df-opab
StepHypRef Expression
1 wph . . 3
2 vx . . 3
3 vy . . 3
41, 2, 3copab 4509 . 2
5 vz . . . . . . . 8
65cv 1394 . . . . . . 7
72cv 1394 . . . . . . . 8
83cv 1394 . . . . . . . 8
97, 8cop 4035 . . . . . . 7
106, 9wceq 1395 . . . . . 6
1110, 1wa 369 . . . . 5
1211, 3wex 1612 . . . 4
1312, 2wex 1612 . . 3
1413, 5cab 2442 . 2
154, 14wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  opabss  4513  opabbid  4514  nfopab  4517  nfopab1  4518  nfopab2  4519  cbvopab  4520  cbvopab1  4522  cbvopab2  4523  cbvopab1s  4524  cbvopab2v  4526  unopab  4527  opabid  4759  elopab  4760  ssopab2  4778  iunopab  4788  dfid3  4801  elxpi  5020  rabxp  5041  csbxp  5086  csbxpgOLD  5087  relopabi  5133  opabbrexOLD  6340  dfoprab2  6343  dmoprab  6383  opabex2  6738  dfopab2  6854  brdom7disj  8930  brdom6disj  8931  swrd0  12658  cnvoprab  27546  areacirc  30112  dropab1  31356  dropab2  31357  csbxpgVD  33694  relopabVD  33701
  Copyright terms: Public domain W3C validator