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

Definition df-opab 3975
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 4204 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 6026. For example,  R  =  { <. x ,  y
>.  |  ( x  e.  CC  /\  y  e.  CC  /\  ( x  +  1 )  =  y ) }  ->  3 R 4 (ex-opab 20632). (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 3973 . 2  class  { <. x ,  y >.  |  ph }
5 vz . . . . . . . 8  set  z
65cv 1618 . . . . . . 7  class  z
72cv 1618 . . . . . . . 8  class  x
83cv 1618 . . . . . . . 8  class  y
97, 8cop 3547 . . . . . . 7  class  <. x ,  y >.
106, 9wceq 1619 . . . . . 6  wff  z  = 
<. x ,  y >.
1110, 1wa 360 . . . . 5  wff  ( z  =  <. x ,  y
>.  /\  ph )
1211, 3wex 1537 . . . 4  wff  E. y
( z  =  <. x ,  y >.  /\  ph )
1312, 2wex 1537 . . 3  wff  E. x E. y ( z  = 
<. x ,  y >.  /\  ph )
1413, 5cab 2239 . 2  class  { z  |  E. x E. y ( z  = 
<. x ,  y >.  /\  ph ) }
154, 14wceq 1619 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  3977  opabbid  3978  nfopab  3981  nfopab1  3982  nfopab2  3983  cbvopab  3984  cbvopab1  3986  cbvopab2  3987  cbvopab1s  3988  cbvopab2v  3990  unopab  3992  opabid  4164  elopab  4165  ssopab2  4183  iunopab  4189  dfid3  4203  elxpi  4612  csbxpg  4623  rabxp  4632  relopabi  4718  dfoprab2  5747  dmoprab  5780  dfopab2  6026  brdom7disj  8040  brdom6disj  8041  dropab1  26817  dropab2  26818  csbxpgVD  27457  relopabVD  27464
  Copyright terms: Public domain W3C validator