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

Definition df-opab 4201
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 4434 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 6333. For example,  R  =  { <. x ,  y
>.  |  ( x  e.  CC  /\  y  e.  CC  /\  ( x  +  1 )  =  y ) }  ->  3 R 4 (ex-opab 21581). (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  set  x
3 vy . . 3  set  y
41, 2, 3copab 4199 . 2  class  { <. x ,  y >.  |  ph }
5 vz . . . . . . . 8  set  z
65cv 1648 . . . . . . 7  class  z
72cv 1648 . . . . . . . 8  class  x
83cv 1648 . . . . . . . 8  class  y
97, 8cop 3753 . . . . . . 7  class  <. x ,  y >.
106, 9wceq 1649 . . . . . 6  wff  z  = 
<. x ,  y >.
1110, 1wa 359 . . . . 5  wff  ( z  =  <. x ,  y
>.  /\  ph )
1211, 3wex 1547 . . . 4  wff  E. y
( z  =  <. x ,  y >.  /\  ph )
1312, 2wex 1547 . . 3  wff  E. x E. y ( z  = 
<. x ,  y >.  /\  ph )
1413, 5cab 2366 . 2  class  { z  |  E. x E. y ( z  = 
<. x ,  y >.  /\  ph ) }
154, 14wceq 1649 1  wff  { <. x ,  y >.  |  ph }  =  { z  |  E. x E. y
( z  =  <. x ,  y >.  /\  ph ) }
Colors of variables: wff set class
This definition is referenced by:  opabss  4203  opabbid  4204  nfopab  4207  nfopab1  4208  nfopab2  4209  cbvopab  4210  cbvopab1  4212  cbvopab2  4213  cbvopab1s  4214  cbvopab2v  4216  unopab  4218  opabid  4395  elopab  4396  ssopab2  4414  iunopab  4420  dfid3  4433  elxpi  4827  csbxpg  4838  rabxp  4847  relopabi  4933  opabbrex  6050  dfoprab2  6053  dmoprab  6086  dfopab2  6333  brdom7disj  8335  brdom6disj  8336  areacirc  25981  dropab1  27311  dropab2  27312  csbxpgVD  28340  relopabVD  28347
  Copyright terms: Public domain W3C validator