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

Definition df-opab 4078
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 6174. For example,  R  =  { <. x ,  y
>.  |  ( x  e.  CC  /\  y  e.  CC  /\  ( x  +  1 )  =  y ) }  ->  3 R 4 (ex-opab 20819). (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 4076 . 2  class  { <. x ,  y >.  |  ph }
5 vz . . . . . . . 8  set  z
65cv 1622 . . . . . . 7  class  z
72cv 1622 . . . . . . . 8  class  x
83cv 1622 . . . . . . . 8  class  y
97, 8cop 3643 . . . . . . 7  class  <. x ,  y >.
106, 9wceq 1623 . . . . . 6  wff  z  = 
<. x ,  y >.
1110, 1wa 358 . . . . 5  wff  ( z  =  <. x ,  y
>.  /\  ph )
1211, 3wex 1528 . . . 4  wff  E. y
( z  =  <. x ,  y >.  /\  ph )
1312, 2wex 1528 . . 3  wff  E. x E. y ( z  = 
<. x ,  y >.  /\  ph )
1413, 5cab 2269 . 2  class  { z  |  E. x E. y ( z  = 
<. x ,  y >.  /\  ph ) }
154, 14wceq 1623 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  4080  opabbid  4081  nfopab  4084  nfopab1  4085  nfopab2  4086  cbvopab  4087  cbvopab1  4089  cbvopab2  4090  cbvopab1s  4091  cbvopab2v  4093  unopab  4095  opabid  4271  elopab  4272  ssopab2  4290  iunopab  4296  dfid3  4310  elxpi  4705  csbxpg  4716  rabxp  4725  relopabi  4811  dfoprab2  5895  dmoprab  5928  dfopab2  6174  brdom7disj  8156  brdom6disj  8157  areacirc  24931  dropab1  27650  dropab2  27651  csbxpgVD  28670  relopabVD  28677
  Copyright terms: Public domain W3C validator