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

Definition df-opab 4038
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 4269 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 6094. For example,  R  =  { <. x ,  y
>.  |  ( x  e.  CC  /\  y  e.  CC  /\  ( x  +  1 )  =  y ) }  ->  3 R 4 (ex-opab 20748). (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 4036 . 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 3603 . . . . . . 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 2242 . 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  4040  opabbid  4041  nfopab  4044  nfopab1  4045  nfopab2  4046  cbvopab  4047  cbvopab1  4049  cbvopab2  4050  cbvopab1s  4051  cbvopab2v  4053  unopab  4055  opabid  4229  elopab  4230  ssopab2  4248  iunopab  4254  dfid3  4268  elxpi  4679  csbxpg  4690  rabxp  4699  relopabi  4785  dfoprab2  5815  dmoprab  5848  dfopab2  6094  brdom7disj  8110  brdom6disj  8111  dropab1  27004  dropab2  27005  csbxpgVD  27704  relopabVD  27711
  Copyright terms: Public domain W3C validator