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

Definition df-opab 4227
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 4460 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 6360. For example,  R  =  { <. x ,  y
>.  |  ( x  e.  CC  /\  y  e.  CC  /\  ( x  +  1 )  =  y ) }  ->  3 R 4 (ex-opab 21693). (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 4225 . 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 3777 . . . . . . 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 2390 . 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  4229  opabbid  4230  nfopab  4233  nfopab1  4234  nfopab2  4235  cbvopab  4236  cbvopab1  4238  cbvopab2  4239  cbvopab1s  4240  cbvopab2v  4242  unopab  4244  opabid  4421  elopab  4422  ssopab2  4440  iunopab  4446  dfid3  4459  elxpi  4853  csbxpg  4864  rabxp  4873  relopabi  4959  opabbrex  6077  dfoprab2  6080  dmoprab  6113  dfopab2  6360  brdom7disj  8365  brdom6disj  8366  areacirc  26187  dropab1  27517  dropab2  27518  csbxpgVD  28715  relopabVD  28722
  Copyright terms: Public domain W3C validator