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

Definition df-opab 4080
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 4311 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 6136. For example,  R  =  { <. x ,  y
>.  |  ( x  e.  CC  /\  y  e.  CC  /\  ( x  +  1 )  =  y ) }  ->  3 R 4 (ex-opab 20795). (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 4078 . 2  class  { <. x ,  y >.  |  ph }
5 vz . . . . . . . 8  set  z
65cv 1623 . . . . . . 7  class  z
72cv 1623 . . . . . . . 8  class  x
83cv 1623 . . . . . . . 8  class  y
97, 8cop 3645 . . . . . . 7  class  <. x ,  y >.
106, 9wceq 1624 . . . . . 6  wff  z  = 
<. x ,  y >.
1110, 1wa 360 . . . . 5  wff  ( z  =  <. x ,  y
>.  /\  ph )
1211, 3wex 1529 . . . 4  wff  E. y
( z  =  <. x ,  y >.  /\  ph )
1312, 2wex 1529 . . 3  wff  E. x E. y ( z  = 
<. x ,  y >.  /\  ph )
1413, 5cab 2271 . 2  class  { z  |  E. x E. y ( z  = 
<. x ,  y >.  /\  ph ) }
154, 14wceq 1624 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  4082  opabbid  4083  nfopab  4086  nfopab1  4087  nfopab2  4088  cbvopab  4089  cbvopab1  4091  cbvopab2  4092  cbvopab1s  4093  cbvopab2v  4095  unopab  4097  opabid  4271  elopab  4272  ssopab2  4290  iunopab  4296  dfid3  4310  elxpi  4705  csbxpg  4716  rabxp  4725  relopabi  4811  dfoprab2  5857  dmoprab  5890  dfopab2  6136  brdom7disj  8152  brdom6disj  8153  dropab1  27050  dropab2  27051  csbxpgVD  27939  relopabVD  27946
  Copyright terms: Public domain W3C validator