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

Definition df-opab 4478
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 4774 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 6879. For example,  R  =  { <. x ,  y >.  |  ( x  e.  CC  /\  y  e.  CC  /\  ( x  +  1 )  =  y ) }  ->  3 R 4 (ex-opab 25938). (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  setvar  x
3 vy . . 3  setvar  y
41, 2, 3copab 4476 . 2  class  { <. x ,  y >.  |  ph }
5 vz . . . . . . . 8  setvar  z
65cv 1454 . . . . . . 7  class  z
72cv 1454 . . . . . . . 8  class  x
83cv 1454 . . . . . . . 8  class  y
97, 8cop 3986 . . . . . . 7  class  <. x ,  y >.
106, 9wceq 1455 . . . . . 6  wff  z  = 
<. x ,  y >.
1110, 1wa 375 . . . . 5  wff  ( z  =  <. x ,  y
>.  /\  ph )
1211, 3wex 1674 . . . 4  wff  E. y
( z  =  <. x ,  y >.  /\  ph )
1312, 2wex 1674 . . 3  wff  E. x E. y ( z  = 
<. x ,  y >.  /\  ph )
1413, 5cab 2448 . 2  class  { z  |  E. x E. y ( z  = 
<. x ,  y >.  /\  ph ) }
154, 14wceq 1455 1  wff  { <. x ,  y >.  |  ph }  =  { z  |  E. x E. y
( z  =  <. x ,  y >.  /\  ph ) }
Colors of variables: wff setvar class
This definition is referenced by:  opabss  4480  opabbid  4481  nfopab  4484  nfopab1  4485  nfopab2  4486  cbvopab  4487  cbvopab1  4489  cbvopab2  4490  cbvopab1s  4491  cbvopab2v  4493  unopab  4494  opabid  4725  elopab  4726  ssopab2  4744  iunopab  4754  dfid3  4772  elxpi  4872  rabxp  4893  csbxp  4938  relopabi  4981  opabbrexOLD  6363  dfoprab2  6369  dmoprab  6409  opabex2  6763  dfopab2  6879  brdom7disj  8990  brdom6disj  8991  cnvoprab  28360  areacirc  32083  dropab1  36845  dropab2  36846  csbxpgOLD  37255  csbxpgVD  37332  relopabVD  37339
  Copyright terms: Public domain W3C validator