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

Definition df-opab 4259
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 4492 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 6393. For example,  R  =  { <. x ,  y
>.  |  ( x  e.  CC  /\  y  e.  CC  /\  ( x  +  1 )  =  y ) }  ->  3 R 4 (ex-opab 21732). (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 4257 . 2  class  { <. x ,  y >.  |  ph }
5 vz . . . . . . . 8  set  z
65cv 1651 . . . . . . 7  class  z
72cv 1651 . . . . . . . 8  class  x
83cv 1651 . . . . . . . 8  class  y
97, 8cop 3809 . . . . . . 7  class  <. x ,  y >.
106, 9wceq 1652 . . . . . 6  wff  z  = 
<. x ,  y >.
1110, 1wa 359 . . . . 5  wff  ( z  =  <. x ,  y
>.  /\  ph )
1211, 3wex 1550 . . . 4  wff  E. y
( z  =  <. x ,  y >.  /\  ph )
1312, 2wex 1550 . . 3  wff  E. x E. y ( z  = 
<. x ,  y >.  /\  ph )
1413, 5cab 2421 . 2  class  { z  |  E. x E. y ( z  = 
<. x ,  y >.  /\  ph ) }
154, 14wceq 1652 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  4261  opabbid  4262  nfopab  4265  nfopab1  4266  nfopab2  4267  cbvopab  4268  cbvopab1  4270  cbvopab2  4271  cbvopab1s  4272  cbvopab2v  4274  unopab  4276  opabid  4453  elopab  4454  ssopab2  4472  iunopab  4478  dfid3  4491  elxpi  4886  csbxpg  4897  rabxp  4906  relopabi  4992  opabbrex  6110  dfoprab2  6113  dmoprab  6146  dfopab2  6393  brdom7disj  8401  brdom6disj  8402  areacirc  26288  dropab1  27617  dropab2  27618  csbxpgVD  28943  relopabVD  28950
  Copyright terms: Public domain W3C validator