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

Definition df-opab 4485
Description: Define the class abstraction of a collection of ordered pairs. Definition 3.3 of [Monk1] p. 34. Usually  x and  y are distinct, although the definition doesn't strictly require it (see dfid2 4772 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 6861. For example,  R  =  { <. x ,  y >.  |  ( x  e.  CC  /\  y  e.  CC  /\  ( x  +  1 )  =  y ) }  ->  3 R 4 (ex-opab 25727). (Contributed by NM, 4-Jul-1994.)
Assertion
Ref Expression
df-opab  |-  { <. x ,  y >.  |  ph }  =  { z  |  E. x E. y
( z  =  <. x ,  y >.  /\  ph ) }
Distinct variable groups:    x, z    y, z    ph, z
Allowed substitution hints:    ph( x, y)

Detailed syntax breakdown of Definition df-opab
StepHypRef Expression
1 wph . . 3  wff  ph
2 vx . . 3  setvar  x
3 vy . . 3  setvar  y
41, 2, 3copab 4483 . 2  class  { <. x ,  y >.  |  ph }
5 vz . . . . . . . 8  setvar  z
65cv 1436 . . . . . . 7  class  z
72cv 1436 . . . . . . . 8  class  x
83cv 1436 . . . . . . . 8  class  y
97, 8cop 4008 . . . . . . 7  class  <. x ,  y >.
106, 9wceq 1437 . . . . . 6  wff  z  = 
<. x ,  y >.
1110, 1wa 370 . . . . 5  wff  ( z  =  <. x ,  y
>.  /\  ph )
1211, 3wex 1659 . . . 4  wff  E. y
( z  =  <. x ,  y >.  /\  ph )
1312, 2wex 1659 . . 3  wff  E. x E. y ( z  = 
<. x ,  y >.  /\  ph )
1413, 5cab 2414 . 2  class  { z  |  E. x E. y ( z  = 
<. x ,  y >.  /\  ph ) }
154, 14wceq 1437 1  wff  { <. x ,  y >.  |  ph }  =  { z  |  E. x E. y
( z  =  <. x ,  y >.  /\  ph ) }
Colors of variables: wff setvar class
This definition is referenced by:  opabss  4487  opabbid  4488  nfopab  4491  nfopab1  4492  nfopab2  4493  cbvopab  4494  cbvopab1  4496  cbvopab2  4497  cbvopab1s  4498  cbvopab2v  4500  unopab  4501  opabid  4728  elopab  4729  ssopab2  4747  iunopab  4757  dfid3  4770  elxpi  4870  rabxp  4891  csbxp  4936  relopabi  4979  opabbrexOLD  6348  dfoprab2  6351  dmoprab  6391  opabex2  6745  dfopab2  6861  brdom7disj  8957  brdom6disj  8958  cnvoprab  28151  areacirc  31740  dropab1  36436  dropab2  36437  csbxpgOLD  36853  csbxpgVD  36930  relopabVD  36937
  Copyright terms: Public domain W3C validator