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

Definition df-opab 4496
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 4787 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 6839. For example,  R  =  { <. x ,  y >.  |  ( x  e.  CC  /\  y  e.  CC  /\  ( x  +  1 )  =  y ) }  ->  3 R 4 (ex-opab 25131). (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 4494 . 2  class  { <. x ,  y >.  |  ph }
5 vz . . . . . . . 8  setvar  z
65cv 1382 . . . . . . 7  class  z
72cv 1382 . . . . . . . 8  class  x
83cv 1382 . . . . . . . 8  class  y
97, 8cop 4020 . . . . . . 7  class  <. x ,  y >.
106, 9wceq 1383 . . . . . 6  wff  z  = 
<. x ,  y >.
1110, 1wa 369 . . . . 5  wff  ( z  =  <. x ,  y
>.  /\  ph )
1211, 3wex 1599 . . . 4  wff  E. y
( z  =  <. x ,  y >.  /\  ph )
1312, 2wex 1599 . . 3  wff  E. x E. y ( z  = 
<. x ,  y >.  /\  ph )
1413, 5cab 2428 . 2  class  { z  |  E. x E. y ( z  = 
<. x ,  y >.  /\  ph ) }
154, 14wceq 1383 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  4498  opabbid  4499  nfopab  4502  nfopab1  4503  nfopab2  4504  cbvopab  4505  cbvopab1  4507  cbvopab2  4508  cbvopab1s  4509  cbvopab2v  4511  unopab  4512  opabid  4744  elopab  4745  ssopab2  4763  iunopab  4773  dfid3  4786  elxpi  5005  rabxp  5026  csbxp  5071  csbxpgOLD  5072  relopabi  5118  opabbrexOLD  6325  dfoprab2  6328  dmoprab  6368  opabex2  6723  dfopab2  6839  brdom7disj  8912  brdom6disj  8913  swrd0  12640  cnvoprab  27524  areacirc  30088  dropab1  31310  dropab2  31311  csbxpgVD  33562  relopabVD  33569
  Copyright terms: Public domain W3C validator