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

Definition df-opab 4094
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 4327 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 6190. For example,  R  =  { <. x ,  y
>.  |  ( x  e.  CC  /\  y  e.  CC  /\  ( x  +  1 )  =  y ) }  ->  3 R 4 (ex-opab 20835). (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 4092 . 2  class  { <. x ,  y >.  |  ph }
5 vz . . . . . . . 8  set  z
65cv 1631 . . . . . . 7  class  z
72cv 1631 . . . . . . . 8  class  x
83cv 1631 . . . . . . . 8  class  y
97, 8cop 3656 . . . . . . 7  class  <. x ,  y >.
106, 9wceq 1632 . . . . . 6  wff  z  = 
<. x ,  y >.
1110, 1wa 358 . . . . 5  wff  ( z  =  <. x ,  y
>.  /\  ph )
1211, 3wex 1531 . . . 4  wff  E. y
( z  =  <. x ,  y >.  /\  ph )
1312, 2wex 1531 . . 3  wff  E. x E. y ( z  = 
<. x ,  y >.  /\  ph )
1413, 5cab 2282 . 2  class  { z  |  E. x E. y ( z  = 
<. x ,  y >.  /\  ph ) }
154, 14wceq 1632 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  4096  opabbid  4097  nfopab  4100  nfopab1  4101  nfopab2  4102  cbvopab  4103  cbvopab1  4105  cbvopab2  4106  cbvopab1s  4107  cbvopab2v  4109  unopab  4111  opabid  4287  elopab  4288  ssopab2  4306  iunopab  4312  dfid3  4326  elxpi  4721  csbxpg  4732  rabxp  4741  relopabi  4827  dfoprab2  5911  dmoprab  5944  dfopab2  6190  brdom7disj  8172  brdom6disj  8173  areacirc  25034  dropab1  27753  dropab2  27754  opabbrex  28191  csbxpgVD  28986  relopabVD  28993
  Copyright terms: Public domain W3C validator